PV3 ⊧ SecCchecks user-specified information flow properties of C code

"A prototype program verification tool for proving information flow security of C code."

Application domain/field

• Software verification
• Information flow properties
• Security verification

Type of tool

Deductive verifier? Auto-active verifier?

Expected input

• Program
• Information flow property (assertions in SecCSL)

Format:

C file

Internals

An automatic verifier (for a subset of C) for SecCSL. SecCSL (Security Concurrent Separation Logic) is used to specify data-dependent information flow security properties of low-level programs. SecC reasons about a program using symbolic execution, similar to Verifast and Viper.

Comments

The underlying logic, SecCSL, has been proven sound with Isabelle/HOL.