Pifthon: A Compile-Time Information Flow Analyzer For An Imperative Language
This work addresses usability and precision issues in information flow analysis for programming languages, which is crucial for protecting data confidentiality and integrity in real application development, though it appears incremental as it builds on existing hybrid labeling methods.
The authors tackled the problem of imprecise and hard-to-use compile-time information flow analysis tools by proposing a hybrid labeling approach for an imperative language, resulting in Pifthon, an analyzer for PyX that reduces labeling overhead and covers termination- and progress-sensitive channels while being proven sound under non-interference.
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.