PV4 ⊧ IFC-BMCchecks 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
• Maximum unrolling bound

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

• Procedure for bounded verification of secure information flow.
• Implemented on top of SeaHorn, uses Z3.
• Note that the paper calls this a 'prototype implementation'.