Paper Info
Title
Proof-Carrying Apps: Contract-Based Deployment-Time Verification.
Abstract
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. With proof-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.
Year
DOI
Venue
2016
10.1007/978-3-319-47166-2_58
Lecture Notes in Computer Science
Keywords
Field
DocType
Deployment-time verification,Design-by-contract,Software evolution
Software deployment,Software engineering,Computer science,Design by contract,Mathematical proof,Software,Software evolution,Extensibility,Formal verification
Conference
Volume
ISSN
Citations 
9952
0302-9743
1
PageRank 
References 
Authors
0.36
16
4
Name
Order
Citations
PageRank
Sönke Holthusen1663.68
Michael Nieke221.74
Thomas Thüm3104847.15
Ina Schaefer4163499.16