loading...
Eliminating Covert Flows with Minimum Typings
Rockport, Massachusetts June 10-June 12
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/CSFW.1997.59680710th Computer Security Foundations Wo ...
 This Article 
 
PDF
HTML
 
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
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.
Citation:
Dennis Volpano, Geoffrey Smith, "Eliminating Covert Flows with Minimum Typings," csfw, pp.156, 10th Computer Security Foundations Workshop (CSFW '97), 1997
Usage of this product signifies your acceptance of the Terms of Use.