Short Paper: Towards Information Flow Reasoning about Real-World C Code.
CCS '17: 2017 ACM SIGSAC Conference on Computer and Communications Security Dallas Texas USA October, 2017(2017)
摘要
Strangely, despite much recent success proving information flow control (IFC) security for C programs, little work has investigated how to prove IFC security directly against C code, as opposed to over an abstract specification. We consider what a suitable IFC logic for C might look like, and propose a suitable continuation-passing style IFC security definition for C code. We discuss our ongoing work implementing these ideas in the context of an existing full-featured, sound program verification framework for C, the Verified Software Toolchain, supported by the verified C complier CompCert.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络