PV4 IFC-CEGARchecks 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 indicating the secret variables 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

https://doi.org/10.1007/978-3-319-96142-2_11 (CAV 2018)

Last publication date

18 July 2018

Related tools

IFC-BMC

ProVerB specific

View/edit source (Markdown)



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