Título: Information flow in a Java intermediate language
Autores: Ahmedani, Ahmer.
Fecha: 2006
Publicador: McGill University - MCGILL
Fuente:
Tipo: Electronic Thesis or Dissertation
Tema: Computer Science.
Descripción: It is a common practice to retrieve code from an outside source, execute it and return the result to the user. During execution secure data can enter the program by user input or access of a data resource. It is important to track the secure data once it enters the program to identify possible information flows to unwanted regions of the code which would permit undesirable data output to a user. Most approaches to restrict information flow in programs have fallen short of providing a practical solution for mainstream programming languages.
To address this issue, this thesis presents two context-sensitive inter-procedural analyses which analyze an intermediate representation of Java Bytecode for secure information flow. The first analysis assumes that there is only one instance of all class fields where as the second analysis uses points-to information to differentiate between instance fields which belong to different instances of the same class. The analyses track secure information in the program by maintaining sets of secure data. The analyses resolve dynamic method resolution in Java statically by analyzing all possible methods which may be invoked at a call site and merging the secure data sets. We were able to define rules to analyze all the statements in the intermediate representation and also accounted for Java libraries. The analyses do not expect any security annotations in the program.
Type information is useful in debugging, guiding optimizations, and specifying and providing safety proofs for programs. A type system for a subset of the Java Bytecode intermediate representation is also formulated in this thesis. An operational semantics is specified and a type preservation proof assures the soundness of the type system.
Non-trivial benchmarks were analyzed and explicit and implicit information flows were counted for both analyses. The empirical data collected suggests secure data is used in many statements of programs and output of data to a user at several places in a program can lead to information flow if the user does not have the right permission to observe the data.
Idioma: en