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

Application domain/field

• Security verification
• Information flow

Type of tool

Model checker?

Expected input

• Program
• Set of high-security variables

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

• Procedure for unbounded verification of secure information flow. It uses taint analysis and self-composition.
• Implemented on top of SeaHorn, uses Spacer (Z3's CHC solver).
• Note that the paper calls this a 'prototype implementation'.