Proof-Carrying Apps: Contract-Based Deployment-Time Verification
Proof-Carrying Apps: Contract-Based Deployment-Time Verification
复制标题
携带证明的应用程序：基于合同的部署时验证
DOI：
10.1007/978-3-319-47166-2_58
复制
发表时间：
2016
期刊：
影响因子：
--
通讯作者：
I. Schaefer
中科院分区：
文献类型：
--
作者：
S. Holthusen;M. Nieke;T. Thüm;I. Schaefer
对于安全关键领域中的可扩展软件平台，部署的插件按指定工作非常重要。对于允许第三方添加插件的前景尤其如此。我们提出了一种基于合同的方法来进行部署时验证。每个插件都在对其环境的一组特定假设下保证其功能行为。通过携带证明的应用程序，我们将携带证明的代码从证明推广到促进部署时验证的工件，其中预期行为是通过合同设计的方式指定的。通过证明工件，即使在资源受限的设备上，也可以在部署期间检查应用程序与环境假设的一致性。此过程可防止因意外编程错误以及故意恶意行为而导致的不安全操作。我们讨论了形式验证技术必须满足哪些标准才能适用于携带证明的应用程序，并评估携带证明应用程序的验证工具 KeY 和 Soot。
For extensible software platforms in safety-critical domains, it is important that deployed plug-ins work as specified. This is especially true with the prospect of allowing third parties to add plug-ins. We propose a contract-based approach for deployment-time verification. Every plug-in guarantees its functional behavior under a specific set of assumptions towards its environment. Withproof-carrying apps, we generalize proof-carrying code from proofs to artifacts that facilitate deployment-time verification, where the expected behavior is specified by the means of design-by-contract. With proof artifacts, the conformance of apps to environment assumptions is checked during deployment, even on resource-constrained devices. This procedure prevents unsafe operation by unintended programming mistakes as well as intended malicious behavior. We discuss which criteria a formal verification technique has to fulfill to be applicable to proof-carrying apps and evaluate the verification tools KeY and Soot for proof-carrying apps.
Java 和分布式系统：观察、经验和……愿望清单
DOI：
--
发表时间：
2015
期刊：
Principles and Practice of Programming in Java
影响因子：
--
作者：
Niranjan Suri
通讯作者：
Niranjan Suri
影响因子：
16.6
作者：
Thuem, Thomas;Apel, Sven;Saake, Gunter
通讯作者：
Saake, Gunter
使用路径抽象进行高效增量静态分析
DOI：
--
发表时间：
2014
期刊：
Fundamental Approaches to Software Engineering
影响因子：
--
作者：
Rashmi Mudduluru;M. Ramanathan
通讯作者：
M. Ramanathan