secureflow.md

layout: plugin
title: SecureFlow
description: Information flow analysis
key: derived
distrib_mode: proprietary

Overview

SecureFlow is a security-oriented plug-in aimed at verifying that the values of private memory locations cannot influence the values of public locations, i.e. that there are no information leaks in the program.

Usage

In order to take advantage of the plug-in, the main locations of the program must be annotated with ACSL attributes /*@ public */ and /*@ private */. SecureFlow will then build upon the results of Eva and From plug-ins to check that an expression that gets stored into a public location does not depend on any private location.

Dependencies

This plug-in depends on results of the Eva and From plug-ins.