A certified lightweight non-interference Java']Java bytecode verifier

被引:10
作者
Barthe, Gilles [1 ]
Pichardie, David [2 ]
Rezk, Tamara [3 ]
机构
[1] IMDEA Software Inst, Madrid 28660, Spain
[2] INRIA Rennes Bretagne Atlantique, F-35042 Rennes, France
[3] INRIA Sophia Antipolis Mediterranee, F-06902 Sophia Antipolis, France
关键词
TYPED ASSEMBLY LANGUAGE; INFORMATION-FLOW; SYSTEM;
D O I
10.1017/S0960129512000850
中图分类号
TP301 [理论、方法];
学科分类号
081202 ;
摘要
Non-interference guarantees the absence of illicit information flow throughout program execution. It can be enforced by appropriate information flow type systems. Much of the previous work on type systems for non-interference has focused on calculi or high-level programming languages, and existing type systems for low-level languages typically omit objects, exceptions and method calls. We define an information flow type system for a sequential JVM-like language that includes all these programming features, and we prove, in the Coq proof assistant, that it guarantees non-interference. An additional benefit of the formalisation is that we have extracted from our proof a certified lightweight bytecode verifier for information flow. Our work provides, to the best of our knowledge, the first sound and certified information flow type system for such an expressive fragment of the JVM.
引用
收藏
页码:1032 / 1081
页数:50
相关论文
共 42 条
[1]  
Abadi M., 1999, Conference Record of POPL '99. 26th ACM SIGPLAN-SIGACT. Symposium on Principles of Programming Languages, P147, DOI 10.1145/292540.292555
[2]  
Agat J., 2000, THESIS CHALMERS U TE
[3]   A logic for information flow in object-oriented programs [J].
Amtoft, T ;
Bandhakavi, S ;
Banerjee, A .
ACM SIGPLAN NOTICES, 2006, 41 (01) :91-102
[4]   Foundational proof-carrying code [J].
Appel, AW .
16TH ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, PROCEEDINGS, 2001, :247-256
[5]  
Askarov A, 2005, LECT NOTES COMPUT SC, V3679, P197
[6]  
Aydemir BE, 2005, LECT NOTES COMPUT SC, V3603, P50
[7]   Stack-based access control and secure information flow [J].
Banerjee, A ;
Naumann, DA .
JOURNAL OF FUNCTIONAL PROGRAMMING, 2005, 15 :131-177
[8]  
Barthe G, 2004, LECT NOTES COMPUT SC, V2937, P2
[9]  
Barthe G., 2011, LECT NOTES COMPUTER, V7173, P73
[10]   Tractable enforcement of declassification policies [J].
Barthe, Gilles ;
Cavadini, Salvador ;
Rezk, Tamara .
CSF 2008: 21ST IEEE COMPUTER SECURITY FOUNDATIONS SYMPOSIUM, PROCEEDINGS, 2008, :83-97