Robust and compositional verification of object capability patterns
Robust and compositional verification of object capability patterns
复制标题
对象能力模式的稳健和组合验证
DOI：
10.1145/3133913
复制
发表时间：
2017
影响因子：
--
通讯作者：
Derek Dreyer
中科院分区：
文献类型：
--
作者：
David Swasey;Deepak Garg;Derek Dreyer
在Web编程等场景中，代码从多个来源链接在一起，对象能力模式(OCP)提供了基本的保障，使程序员能够保护其对象的私有状态不受未知和不受信任的代码的破坏。然而，OCP在程序验证方面的好处从未得到适当的正式确定。在本文中，我们在最近开发的IRIS并发分离逻辑框架的基础上，开发了OCPL，这是第一个用具有闭包、可变状态和并发的语言来成分地描述和验证OCP的程序逻辑。OCPL的核心思想是通过借鉴安全协议验证文献中的一个著名的思想，即健壮安全，来说明已验证代码和不可信代码之间的接口。只将正确包装的值导出到其环境中的程序可以被证明是非常安全的，这意味着其不受信任的环境不能违反其内部不变量。我们使用OCPL为几个常用的OCP提供第一个通用的、组成的和机器检查的规范--包括动态密封、膜和管理员模式--然后我们使用这些规范来验证典型客户端代码的健壮安全性。我们所有的结果都在Coq证明助手中完全机械化。
In scenarios such as web programming, where code is linked together from multiple sources,object capability patterns(OCPs) provide an essential safeguard, enabling programmers to protect the private state of their objects from corruption by unknown and untrusted code. However, the benefits of OCPs in terms of program verification have never been properly formalized. In this paper, building on the recently developed Iris framework for concurrent separation logic, we develop OCPL, the first program logic for compositionally specifying and verifying OCPs in a language with closures, mutable state, and concurrency. The key idea of OCPL is to account for the interface between verified and untrusted code by adopting a well-known idea from the literature on security protocol verification, namelyrobust safety. Programs that export only properly wrapped values to their environment can be proven robustly safe, meaning that their untrusted environment cannot violate their internal invariants. We use OCPL to give the first general, compositional, and machine-checked specs for several commonly-used OCPs—including thedynamic sealing,membrane, andcaretakerpatterns—which we then use to verify robust safety for representative client code. All our results are fully mechanized in the Coq proof assistant.
登录
查看更多内容
值得信赖的代理 - 具有不变量的虚拟化对象
DOI：
10.1007/978-3-642-39038-8_7
发表时间：
2013
期刊：
Proceedings 2022 Network and Distributed System Security Symposium
影响因子：
--
作者：
T. V. Cutsem;Mark S. Miller
通讯作者：
Mark S. Miller
基于状态的所有权、重入和封装
影响因子：
--
作者：
A. Banerjee;D. Naumann
通讯作者：
D. Naumann
Oz-E 项目：安全多范式编程语言的设计指南
DOI：
10.1007/978-3-540-31845-3_3
发表时间：
2004
期刊：
Qsar & Combinatorial Science
影响因子：
--
作者：
Fred Spiessens;P. V. Roy
通讯作者：
P. V. Roy
DOI：
--
发表时间：
2010
期刊：
--
影响因子：
--
作者：
A. Mettler;D. Wagner;T. Close
通讯作者：
A. Mettler;D. Wagner;T. Close
DOI：
--
发表时间：
2010
期刊：
影响因子：
--
作者：
Toby C. Murray
通讯作者：
Toby C. Murray