Pifthon: A Compile-Time Information Flow Analyzer For An Imperative Language

TL;DR

Pifthon is a compile-time analysis tool for Python-like programs that improves precision and usability in detecting information flow violations, supporting a wide range of programs and ensuring security properties.

Contribution

It introduces a hybrid labeling approach for compile-time information flow analysis in imperative languages, specifically implemented for a Python dialect called PyX.

Findings

Reduces labeling overhead for better usability.

Covers termination- and progress-sensitive channels.

Proven sound under non-interference property.

Abstract

Compile-time information flow analysis has been a promising technique for protecting confidentiality and integrity of private data. In the last couple of decades, a large number of information flow security tools in the form of run-time execution-monitors or static type systems have been developed for programming languages to analyze information flow security policies. However, existing flow analysis tools lack in precision and usability, which is the primary reason behind not being widely adopted in real application development. In this paper, we propose a compile-time information flow analysis for an imperative program based on a hybrid (mutable + immutable) labelling approach that enables a user to detect information flow-policy breaches and modify the program to overcome violations. We have developed an information flow security analyzer for a dialect of Python language, PyX, called Pifthon using the said approach. The flow-analyzer aids in identifying possible misuse of the information in sequential PyX programs corresponding to a given information flow policy (IFP). Pifthon has distinct advantages like reduced labelling overhead that ameliorates usability, covers a wide range of PyX programs that include termination-and progress-sensitive channels, in contrast to other approaches in the literature. The proposed flow analysis is proved to be sound under the classical non-interference property. Further, case study and experience in the usage of Pifthon are provided.