Skip to content

Latest commit

 

History

History
144 lines (109 loc) · 6.63 KB

architectural_concepts.md

File metadata and controls

144 lines (109 loc) · 6.63 KB
Raw

Labyrinth Architectural Concepts

Labyrinth takes a straightforward approach to representing and reasoning about policies as expressions in the Algebra of Sets. It does not make use of SMT Solvers or Binary Decision Diagrams.

Each run of Labyrinth performs the following sequence of steps:

To understand these steps, it is help to understand the concept of the Universe, a structure that defines the set-theoretic context in which all processing occurs.

The Universe

Routes

Routes in labyrinth are represented as tuples of integers in an n-dimensional space, defined by the Universe. Each dimension corresponds to a routing concept like source ip address, port, or protocol. Consider the 5-dimensional universe defined in firewall.js. This universe defines the following dimensions:

  • sourceIp - source ip address, represented as an integer in the range from 0 to 0xffffffff.
  • sourcePort - source port in the range from 0 to 65535.
  • destinationIp - destination ip addresss, represented as an integer in the range from 0 to 0xffffffff.
  • destinationPort - destination port in the range from 0 to 65535.
  • protocol - internet protocol number in the range from 0 to 255.

The route (0x0a000002, 49152, 0xab404002, 443, 6) represents a packet

  • originating from port 49152 on ip address 10.0.0.2 (0x0a000002)
  • targeting port 443 at ip address 172.64.64.2 (0xab404002)
  • using protocol number 6 (tcp).

Rules

Rules in labyrinth consist of assertions of membership in sets associated with each dimension in the Universe. Consider the following rule with three assertions:

soureIp: except 10.0.0.0/8
destinationIp: 171.64.64.0/18
destinationPort: 80, 443
protocol: tcp

This rule consists of four explicit assertions:

  • The first assertion corresponds to those source IP addresses outside the 10.0.0.0/8 CIDR block - in other words, those addresses not between 10.0.0.0 and 10.255.255.255. This corresponds two ranges of source IP addresses - those from 0.0.0.0 to 9.255.255.255 and those from 11.0.0.0 to 255.255.255.255. These can be expressed as the integer ranges [0, 0x09ffffff] and [0x0b000000, 0xffffffff].
  • The second assertion corresponds to those destination IP addresses inside the 171.64.64.0/18 CIDR. These are addresses in the integer range [0xab404000, 0xab40bfff].

NOTE about implicit dimension sourcePort.

Parsing Rules

THIS SECTION COMING SOON

Rule parsing and policy analysis are performed in the context of a Universe . . .

Representing Rules

THIS SECTION COMING SOON

Combining Rules

THIS SECTION COMING SOON

Simplification Strategies

Labyrinth uses two expression simplification strategies. The first is to apply basic algebraic identity and domination laws after each union or intersection operation. The second is to perform a prime-implicant elimination using the Quine–McCluskey algorithm

Basic Algebraic Simplifications

The labyrinth set intersection and union operations perform a number of basic algebraic simplifications. In the following, let

  • D denote the set of all values in the domain
  • 0 denote the empty set

Identity

  • A ⋂ D = A
  • A ⋃ 0 = A

Domination

  • A ⋂ 0 = 0
  • A ⋃ D = D

Since the expressions are in disjunctive normal form,

  • any term reduced to 0 is eliminated from the overall disjunction
  • any term reduced to D reduces the entire expression to D
  • any factor reduced to D is eliminated from its conjunction
  • any factor reduced to 0 causes its term to become 0 and be eliminated from the overall conjunction.

Quine–McCluskey Expression Minimization

This strategy combines terms that share the same values on all but on dimension. For example, the following two terms

sourceIp: 10.0.0.0/8
destinationIp: 171.64.64.0/18
destinationPort: 80

sourceIp: 10.0.0.0/8
destinationIp: 171.64.64.0/18
destinationPort: 443

can be combined into a single term:

sourceIp: 10.0.0.0/8
destinationIp: 171.64.64.0/18
destinationPort: 80, 443

The Quine–McCluskey algorithm identifies and combines sets of terms that share the same values on all but one dimension. It repeats this process until no more terms can be combined.

Formatting

THIS SECTION COMING SOON

Report Generation

THIS SECTION COMING SOON

Suggested Reading