2007 Technical Reports

Department of Computing and Information Sciences
Kansas State University

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.