Secure multi-execution through static program transformation: extended version
作者： Frank Piessens , Gilles Barthe , Dominique Devriese , Exequiel Rivas , Juan Manuel Crespo
DOI:
关键词:
摘要: Secure multi-execution (SME) is a dynamic technique to ensure secure information ow. In nutshell, SME enforces security by running one execution of the program per level, and reinterpreting input/output operations w.r.t. their associated level. sound, in sense that under non-interfering, precise, for programs are non-interfering usual sense, semantics coincides with its standard semantics. A further virtue core idea languageindependent; it can be applied broad range languages. downside fact existing implementation techniques require modi cations runtime environment, e.g. browser Web applications. this article, we develop an alternative approach where e ect achieved through transformation, without runtime, thus supporting server-side deployment on web. We show exemplary language code evaluation (modeled after JavaScript's eval) our transformation sound precise. The crux proof simulation between transformed original program. This has been machine-checked using Agda assistant. also report prototype implementations small fragment Python substantial subset JavaScript. extended version paper published at FMOODS/FORTE 2012. It extends conference technical details about formalization proofs. static transformation: Gilles Barthe, Juan Manuel Crespo, Dominique Devriese, Frank Piessens, Exequiel Rivas 1 IMDEA Software Institute, Madrid, Spain 2 IBBT-DistriNet Research Group, KU Leuven, Belgium Abstract. flow. language-independent; modifications effect JavaScript’s JavaScript.This
kuleuven.be 参考文章(26)
Mike Ter Louw, V. N. Venkatakrishnan, Karthik Thotta Ganesh, AdJail: practical enforcement of confidentiality and integrity policies on web advertisements usenix security symposium. pp. 24- 24 ,(2010)
Alejandro Russo, Andrei Sabelfeld, Andrey Chudnov, Tracking information flow in dynamic tree structures european symposium on research in computer security. pp. 86- 103 ,(2009) , 10.1007/978-3-642-04444-1_6
Gregor Richards, Christian Hammer, Brian Burg, Jan Vitek, The Eval That Men Do european conference on object-oriented programming. pp. 52- 78 ,(2011) , 10.1007/978-3-642-22655-7_4
Sergio Maffeis, John C. Mitchell, Ankur Taly, Isolating JavaScript with filters, rewriting, and wrappers european symposium on research in computer security. pp. 505- 522 ,(2009) , 10.1007/978-3-642-04444-1_31
Andrei Sabelfeld, Alejandro Russo, From dynamic to static and back: riding the roller coaster of information-flow control research international andrei ershov memorial conference on perspectives of system informatics. ,vol. 5947, pp. 352- 365 ,(2009) , 10.1007/978-3-642-11486-1_30
Gurvan Le Guernic, David Schmidt, Anindya Banerjee, Confidentiality enforcement using dynamic information flow analyses Kansas State University. ,(2007)
Salvador Cavadini, Secure slices of insecure programs computer and communications security. pp. 112- 122 ,(2008) , 10.1145/1368310.1368329
Thomas H. Austin, Cormac Flanagan, Permissive dynamic information flow analysis acm workshop on programming languages and analysis for security. pp. 3- ,(2010) , 10.1145/1814217.1814220
Dominique Devriese, Frank Piessens, Noninterference through Secure Multi-execution ieee symposium on security and privacy. pp. 109- 124 ,(2010) , 10.1109/SP.2010.15
Nevin Heintze, Jon G. Riecke, The SLam calculus: programming with secrecy and integrity symposium on principles of programming languages. pp. 365- 377 ,(1998) , 10.1145/268946.268976