Efficient type inference for secure information flow
- 10 June 2006
- proceedings article
- Published by Association for Computing Machinery (ACM)
Abstract
This paper describes the design, analysis, and implementation of an efficient algorithm for information flow analysis expressed using a type system. Given a program and an environment of security classes for information accessed by the program, the algorithm checks whether the program is well typed, i.e., there is no information of higher security classes flowing into places of lower security classes according to a lattice of security classes, by inferring the highest or lowest security class as appropriate for each program node. We express the analysis as a set of Datalog-like rules based on the typing and subtyping rules, and we use a systematic method to generate specialized algorithms and data structures directly from the Datalog-like rules. The generated implementation traverses the program multiple times and uses a combination of linked and indexed data structures to represent program nodes, environments, and types. The time complexity of the algorithm is linear in the size of the input program, times the height of the lattice of security classes, plus a small overhead for preprocessing the security classes. This complexity is confirmed through our prototype implementation and experimental evaluation on code generated from high-level specifications for real systems.Keywords
This publication has 18 references indexed in Scilit:
- Modular and Constraint-Based Information Flow Inference for an Object-Oriented LanguagePublished by Springer Nature ,2004
- Java bytecode verification for secure information flowACM SIGPLAN Notices, 2003
- Language-based information-flow securityIEEE Journal on Selected Areas in Communications, 2003
- Checking security of Java bytecode by abstract interpretationPublished by Association for Computing Machinery (ACM) ,2002
- Secrecy by typing in security protocolsPublished by Springer Nature ,1997
- Program derivation by fixed point computationScience of Computer Programming, 1989
- Efficient implementation of lattice operationsACM Transactions on Programming Languages and Systems, 1989
- Finite Differencing of Computable ExpressionsACM Transactions on Programming Languages and Systems, 1982
- Certification of programs for secure information flowCommunications of the ACM, 1977
- A lattice model of secure information flowCommunications of the ACM, 1976