TWISC Summer School 2006

Application of Formal Verification to Software Security

Slides

Examples used for the presentation:

• Verification of a simple sorting algorithm in Coq
• Examples of verification in Hoare logic in Coq can be found here (GCD, string_copy, etc. in examples.v file)
• A paper on verification of memory management using separation logic in Coq (Coq scripts here)
• A short paper on verification of arithmetic functions in SmartMIPS in Coq (Coq scripts not yet available)
• Verification of a simple client-server application in Spin:
  • Basic model
  • Model with DNS
  • Model with spoofed DNS
  • Specification
• A paper on verification of an embedded operating system in Spin
• Needham-Schroeder protocol in Spin:
  • Model
  • Specification