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

Type of tool

Deductive verifier? Auto-active verifier?

Expected input

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.
Security

Links

Last commit date

29 March 2021

Related papers

https://doi.org/10.1007/978-3-030-25543-5_13 (CAV 2019)

Last publication date

12 July 2019

ProVerB specific

View/edit source (Markdown)



ProVerB is a part of SLEBoK. Last updated: July 2022.