Report 2007-1
Report 2007-1.
Automaton-based non-interference monitoring of concurrent programs
by Gurvan le Guernic
Report 2007-2 Verification Condition Generation for Conditional Information Flow by Torben Amtoft and Anindya Banerjee
Report 2007-3
Correctness of Practical Slicing for Modern Program Structures
by Torben Amtoft
Abstract:
Slicing is a program transformation technique with numerous applications, since it allows the user to focus on the parts of a given program that are relevant for a given purpose. Ideally, the sliced program should have the same termination properties as the original program, but to achieve this, the slicing algorithm must include in the slice all commands that influence the guards of potential loops. For practical purposes, so as to keep the slices manageable, it might be better to slice away loops that do not affect the values of relevant variables.
This paper presents foundational work that accomplishes this goal for arbitrary control flow graphs, whereas previous approaches have assumed the presence of a unique end node; therefore, the proposed approach is able to handle the control flow graphs that arise from modern program structures, such as when modeling reactive systems. A slice set is required to be closed under data dependency and under a certain variant of control dependency, called ``weak order dependency''. This allows a crisp correctness proof, based on simulation techniques, for a correctness criterion stating that the observational behavior of the original program must be a \emph{prefix} of the behavior of the sliced program.
Report 2007-4
On Asymptotic Notation with Multiple Variables
by Rodney R. Howell
Abstract:
We show that it is impossible to define big-O notation for functions
on more than one variable in a way that implies the properties
commonly used in algorithm analysis. We also demonstrate that common
definitions do not imply these properties even if the functions within
the big-O notation are restricted to being strictly nondecreasing. We
then propose an alternative definition that does imply these properties
whenever the function within the big-O notation is strictly
nondecreasing.
Report 2007-5
Report 2007-5.
Dynamic Noninterference Analysis Using Context Sensitive Static Analyses
by Gurvan le Guernic
Abstract:
This report proposes a dynamic noninterference analysis for sequential programs. This analysis is well-suited for the development of a monitor enforcing the absence of information flows between the secret inputs and the public outputs of a program. This implies a sound detection of information flows and a sound correction of forbidden flows during the execution. The monitor relies on a dynamic information flow analysis. For unexecuted pieces of code, this dynamic analysis uses any context sensitive static information flow analysis which respects a given set of three hypotheses. The soundness of the overall monitoring mechanism with regard to noninterference enforcement is proved, as well as its higher precision than the automaton-based mechanism proposed in previous work.