Agda formalization of Li and Zhang's flow and path-sensitive information flow analysis

Agda formalization of a static information flow analysis presented in the "Towards a Flow- and Path-Sensitive Information Flow Analysis: Technical Report" paper by Peixuan Li and Danfeng Zhang, which uses a fixed-label type system with dependent types.

Installation

This formalization has been tested using Agda 2.6.3 and the Agda standard library v1.7.2.

Code Structure

The Agda modules are organized according to the following structure:

• Base
  • AssignmentId
  • AST
  • Liveness
  • Predicates
  • SecurityLabels
  • Transformation
  • VariableSet

Module Content

Base

• AST.agda: Definition of the syntax trees for both the bracketed and non-bracketed versions of the source language. (Section 3)

• Transformation.agda: Transformation between bracketed and non-bracketed programs. (Section 4.2)

• SecurityLabels.agda: Definition of the type system's security labels. (Section 5.3)

• AssignmentId.agda: Assignment of unique IDs to each assignment statement of a program. (Section 5.4)

• Liveness.agda: Variable liveness analysis, which is later used in the typing rules. (Section 5.4)

• Predicates.agda: Generation of program state predicates that are true for each assignment statement, also used in the typing rules. (Section 5.4)

• VariableSet.agda: Utility module defining finite sets of program variables.