Formal model of BliME

We here document the machine-checked proof of security of the BliMe taint-tracking policy.

You will find the model itself on Github

You can also find the slides from a talk on this model here.

Modules:

• Low-level CPU model
  • System state
  • Execution model
  • Safety definitions
• Load-store model
  • Instruction operands
  • Memory operations
  • Instructions
  • Execution model
• Model ISA
  • Instruction format
  • Instruction decoder
  • Instruction semantics
• Blindable values
  • Equivalence
  • Redaction
• Memory state
• Multi-domain BliMe
  • Definitions