PV4 IFC-BMCchecks if a program is safe with respect to variables marked secret

Application domain/field

Type of tool

Model checker?

Expected input

Format:

C-program with annotations that indicate which variables are secret and the locations at which leaks should be checked.

Expected output

SAFE, UNSAFE or UNKNOWN

Internals

C Security

Links

Benchmark files: http://www.cs.princeton.edu/~aartig/benchmarks/ifc_bench.zip

Related papers

Lazy Self-composition for Security Verification (CAV 2018)

Last publication date

18 July 2018

Related tools

IFC-CEGAR

ProVerB specific



ProVerB is a part of SLEBoK. Last updated: February 2023.