compiler/io.github.aplcornell.viaduct.security/SecurityLattice

SecurityLattice

class SecurityLattice<T : Lattice<T>>(val confidentialityComponent: T, val integrityComponent: T) : Lattice<SecurityLattice<T>> , TrustLattice<SecurityLattice<T>> , PrettyPrintable

A lattice for information flow security. This is a product lattice with confidentiality and integrity components. Information flows from less restrictive contexts to more restrictive ones.

Elements of T are interpreted as principals.

meet and join talk about information flow.

and and or talk about trust.

Constructors

SecurityLattice

fun <T : Lattice<T>> SecurityLattice(principal: T)

Returns an element with confidentialityComponent and integrityComponent equal to principal.

SecurityLattice

fun <T : Lattice<T>> SecurityLattice(confidentialityComponent: T, integrityComponent: T)

Types

Bounds

class Bounds<T : Lattice<T>>(bounds: BoundedLattice<T>) : BoundedLattice<SecurityLattice<T>> , BoundedTrustLattice<SecurityLattice<T>>

Provides bounds for a SecurityLattice given bounds for T.

Functions

and

open infix override fun and(that: SecurityLattice<T>): SecurityLattice<T>

The least powerful principal that can act for both this and that. This denotes a conjunction of authority.

confidentiality

fun confidentiality(bounds: BoundedLattice<T>): SecurityLattice<T>

Returns an element that represents the confidentiality component.

integrity

fun integrity(bounds: BoundedLattice<T>): SecurityLattice<T>

Returns an element that represents the integrity component.

join

open infix override fun join(that: SecurityLattice<T>): SecurityLattice<T>

The least upper bound of this and that.

meet

open infix override fun meet(that: SecurityLattice<T>): SecurityLattice<T>

The greatest lower bound of this and that.

open infix override fun or(that: SecurityLattice<T>): SecurityLattice<T>

The most powerful principal both this and that can act for. This denotes a disjunction of authority.

swap

fun swap(): SecurityLattice<T>

Switches the confidentiality and integrity components.

toDocument

open override fun toDocument(): Document

toString

open override fun toString(): String

Properties

confidentialityComponent

val confidentialityComponent: T

The confidentiality component in the underlying lattice.

integrityComponent

val integrityComponent: T

The integrity component in the underlying lattice.

Extensions

confidentiality

fun Label.confidentiality(): Label

confidentialityFlowsTo

fun <C : HeytingAlgebra<C>, V, T> Term<C, V>.confidentialityFlowsTo(that: Term<C, V>, bounds: BoundedLattice<C>, failWith: (SecurityLattice<C>, SecurityLattice<C>) -> T): Iterable<Constraint<C, V, T>>

flowsTo

fun <C : HeytingAlgebra<C>, V, T> Term<C, V>.flowsTo(that: Term<C, V>, bounds: BoundedLattice<C>, failWith: (SecurityLattice<C>, SecurityLattice<C>) -> T): Iterable<Constraint<C, V, T>>

Returns a constraint that represents [this] flowsTo [that].

integrity

fun Label.integrity(): Label

integrityFlowsTo

fun <C : HeytingAlgebra<C>, V, T> Term<C, V>.integrityFlowsTo(that: Term<C, V>, bounds: BoundedLattice<C>, failWith: (SecurityLattice<C>, SecurityLattice<C>) -> T): Iterable<Constraint<C, V, T>>