CanFlowTo | SecLib.TCB.Lattice |
H | SecLib.LowHigh |
ioTCB | SecLib.TCB.SecIO |
L | SecLib.LowHigh |
Less | SecLib.TCB.Lattice, SecLib.Lattice |
MkSec | SecLib.TCB.Sec |
MkSecIO | SecLib.TCB.SecIO |
newRefSecIO | SecLib.TCB.Ref, SecLib.Ref |
plug | SecLib.TCB.SecIO, SecLib.SecIO |
public | SecLib.LowHigh |
readRefSecIO | SecLib.TCB.Ref, SecLib.Ref |
Ref | SecLib.TCB.Ref, SecLib.Ref |
reveal | SecLib.Reveal |
run | SecLib.TCB.SecIO, SecLib.SecIO |
Sec | SecLib.TCB.Sec, SecLib.Sec |
SecIO | SecLib.TCB.SecIO, SecLib.SecIO |
toSecIO | SecLib.TCB.SecIO, SecLib.SecIO |
unsec | SecLib.TCB.Sec |
up | SecLib.TCB.Sec, SecLib.Sec |
writeRefSecIO | SecLib.TCB.Ref, SecLib.Ref |