摘要: This paper presents a type-based information flow analysis for call-by-value λ-calculus equipped with references, exceptions and let-polymorphism, which we refer to as ML. The type system is constraint-based has decidable inference. Its noninterference proof reasonably light-weight, thanks the use of number orthogonal techniques. First, syntactic segregation between values expressions allows lighter formulation system. Second, reduced subject reduction nonstandard language extension. Lastly, semi-syntactic approach soundness dealing polymorphism separately.
acm.org
unirioja.es
core.ac.uk
sci-hub.se 参考文章(32)
Manuel Alfred Fahndrich, Alexander Aiken, Bane: a library for scalable constraint-based program analysis University of California, Berkeley. ,(1999)
François Pottier, A Semi-Syntactic Soundness Proof for HM(X) INRIA. ,(2001)
Barbara Liskov, Andrew C. Myers, Mostly-Static Decentralized Information Flow Control Massachusetts Institute of Technology. ,(1999)
Dennis Volpano, Geoffrey Smith, A Type-Based Approach to Program Security colloquium on trees in algebra and programming. pp. 607- 621 ,(1997) , 10.1007/BFB0030629
Steve Zdancewic, Andrew C. Myers, Secure Information Flow via Linear Continuations Higher-Order and Symbolic Computation archive. ,vol. 15, pp. 209- 234 ,(2002) , 10.1023/A:1020843229247
Mads Tofte, Robin Milner, Robert Harper, David MacQueen, The Definition of Standard ML (Revised) MIT Press. ,(1997)
Steve Zdancewic, Andrew C. Myers, Secure Information Flow and CPS european symposium on programming. pp. 46- 61 ,(2001) , 10.1007/3-540-45309-1_4
Mads Tofte, Mads Tofte, Robert Harper, Robin Milner, The Definition of Standard ML ,(1990)
Dorothy Elizabeth Robling Denning, Cryptography and data security ,(1982)
F. Pottier, A simple view of type-secure information flow in the /spl pi/-calculus ieee computer security foundations symposium. pp. 320- 330 ,(2002) , 10.1109/CSFW.2002.1021826