Sentry Formal Proof

Contents:

• Basic principles
  • About Frama-C
  • Frama-C integration in Sentry
  • Impact of formal proofness in kernel design
• Value analysis
  • About EVA
  • EVA integration with Sentry kernel
  • EVA coverage
  • Alarms and reports
• Functional correctness
  • About WP
  • WP and composition-based correctness
  • Correctness of hardware manipulation
  • Correctness of security model