Tech Talk: Verifying C programs in Coq using VST

  • Date Friday, August 08, 2014  Time
  • Speaker Joey Dodds
  • Location Galois, Inc., 421 SW 6th Ave., Suite 300, Portland, OR, USA (3rd floor of the Commonwealth Building)
  • Galois is pleased to host the following tech talk. These talks are free and open to the interested public--please join us! (There is no need to pre-register for the talk.)

    The talk starts at 11:00am.

Abstract

C programs are notoriously difficult to reason about, either for safety or full functional correctness. Even with a program logic powerful enough to prove the necessary properties, the proof has the assumption that the compiler behaves exactly the way it is expected to. Verified Software Toolchain (VST) answers this problem by providing a logic specified at the source level that proves properties about generated assembly code. It is proved sound w.r.t. the operational semantics of C, the same operational semantics compiled by the proved-correct CompCert verified optimizing C compiler. Both of those proofs are machine-checked in Coq, an interactive proof assistant. This talk will present the basics of VST, followed by an example proof of a C program.

Bio

Josiah (Joey) Dodds is an intern at Galois for the summer, researching the verification of cryptographic libraries. After the summer he will return to finish his PhD at Princeton, where he has been verifying information-flow properties and C programs in Coq.