Eliminating covert flows with minimum typings
- 22 November 2002
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- No. 10636900,p. 156-168
- https://doi.org/10.1109/csfw.1997.596807
Abstract
A type system is given that eliminates two kinds of covert flows in an imperative programming language. The first kind arises from nontermination and the other from partial operations that can raise exceptions. The key idea is to limit the source of nontermination in the language to constructs with minimum typings, and to evaluate partial operations within expressions of try commands which also have minimum typings. A mutual progress theorem is proved that basically states that no two executions of a well-typed program can be distinguished on the basis of nontermination versus abnormal termination due to a partial operation. The proof uses a new style of programming language semantics which we call a natural transition semantics.Keywords
This publication has 6 references indexed in Scilit:
- A sound polymorphic type system for a dialect of CScience of Computer Programming, 1998
- A sound type system for secure flow analysisJournal of Computer Security, 1996
- A type soundness proof for variables in LCF MLInformation Processing Letters, 1995
- Formal methods and automated tool for timing-channel identification in tcb source codePublished by Springer Nature ,1992
- An Axiomatic Approach to Information Flow in ProgramsACM Transactions on Programming Languages and Systems, 1980
- Certification of programs for secure information flowCommunications of the ACM, 1977