Sound Modular Verification of C Code Executing in an Unverified Context

被引:0
作者
Agten, Pieter [1 ]
Jacobs, Bart [1 ]
Piessens, Frank [1 ]
机构
[1] Katholieke Univ Leuven, iMinds DistriNet, Leuven, Belgium
基金
比利时弗兰德研究基金会;
关键词
separation logic; verification; runtime checking; CONTRACTS; CHECKING; VCC;
D O I
10.1145/2775051.2676972
中图分类号
TP31 [计算机软件];
学科分类号
081202 ; 0835 ;
摘要
Over the past decade, great progress has been made in the static modular verification of C code by means of separation logic-based program logics. However, the runtime guarantees offered by such verification are relatively limited when the verified modules are part of a whole program that also contains unverified modules. In particular, a memory safety error in an unverified module can corrupt the runtime state, leading to assertion failures or invalid memory accesses in the verified modules. This paper develops runtime checks to be inserted at the boundary between the verified and the unverified part of a program, to guarantee that no assertion failures or invalid memory accesses can occur at runtime in any verified module. One of the key challenges is enforcing the separation logic frame rule, which we achieve by checking the integrity of the footprint of the verified part of the program on each control flow transition from the unverified to the verified part. This in turn requires the presence of some support for module-private memory at runtime. We formalize our approach and prove soundness. We implement the necessary runtime checks by means of a program transformation that translates C code with separation logic annotations into plain C, and that relies on a protected module architecture for providing module-private memory and restricted module entry points. Benchmarks show the performance impact of this transformation depends on the choice of boundary between the verified and unverified parts of the program, but is below 4% for real-world applications.
引用
收藏
页码:581 / 594
页数:14
相关论文
共 37 条
[1]  
Abadi M, 1998, LECT NOTES COMPUT SC, V1443, P868, DOI 10.1007/BFb0055109
[2]  
Agten P., 2014, 676 CW KU LEUV
[3]   Secure Compilation to Modern Processors [J].
Agten, Pieter ;
Strackx, Raoul ;
Jacobs, Bart ;
Piessens, Frank .
2012 IEEE 25TH COMPUTER SECURITY FOUNDATIONS SYMPOSIUM (CSF), 2012, :171-185
[4]  
[Anonymous], 2010, PLTTR20101 INC
[5]  
AUSTIN TM, 1994, SIGPLAN NOTICES, V29, P290, DOI 10.1145/773473.178446
[6]   Runtime verification of .NET contracts [J].
Barnett, M ;
Schulte, W .
JOURNAL OF SYSTEMS AND SOFTWARE, 2003, 65 (03) :199-208
[7]  
Berdine J, 2006, LECT NOTES COMPUT SC, V4111, P115
[8]   An overview of JML tools and applications [J].
Burdy L. ;
Cheon Y. ;
Cok D.R. ;
Ernst M.D. ;
Kiniry J.R. ;
Leavens G.T. ;
Leino K.R.M. ;
Poll E. .
International Journal on Software Tools for Technology Transfer, 2005, 7 (3) :212-232
[9]  
Calcagno C, 2009, LECT NOTES COMPUT SC, V5904, P259, DOI 10.1007/978-3-642-10672-9_19
[10]   Automated verification of shape, size and bag properties via user-defined predicates in separation logic [J].
Chin, Wei-Ngan ;
David, Cristina ;
Huu Hai Nguyen ;
Qin, Shengchao .
SCIENCE OF COMPUTER PROGRAMMING, 2012, 77 (09) :1006-1036