SecLib.TCB.Lattice

Documentation

class CanFlowTo l l'

Instances

CanFlowTo H H

CanFlowTo L H

CanFlowTo L L

class CanFlowTo l l' => Less l l'

The class Less determines the allowed flows of information. Less l l' tests the order relationship of l and l' in the lattice, i.e., if l ⊑ l'.

The sole purpose of the unexported class CanFlowTo is to restrict untrusted code from making arbitrary instances of the class Less (credit to Pablo Buiras!)

Instances

Less H H

Two-point lattice (information can flow between secret entities)

Less L H

Two-point lattice (information can flow from public to secret entities)

Less L L

Two-point lattice (information can flow between public entities)