Automated Verification of RPC Stub Code

Select |




Print


Fernandez, Matthew; Andronick, June; Klein, Gerwin; Kuz, Ihor

Fernandez, Matthew; Andronick, June; Klein, Gerwin; Kuz, Ihor


2015-06-20


Conference Material


International Symposium on Formal Methods


Oslo, Norway


273-290


Formal verification has been successfully applied to provide strong correctness guarantees of software systems, but its application to large code bases remains an open challenge. The technique of component-based software devel- opment, traditionally employed for engineering benefit, also aids reasoning about such systems. While there exist compositional verification techniques that lever- age the separation implied by a component system architecture, they implicitly rely on the component platform correctly implementing the isolation and com- position semantics they assume. Any property proven using these techniques is vulnerable to being invalidated by a bug in the code of the platform itself. In this paper, we show how this assumption can be eliminated by automatically gener- ating machine-checked proofs of the correctness of a component platform’s gen- erated Remote Procedure Call (RPC) code. We demonstrate how these generated proofs can be composed with hand-written proofs to yield a system-level property with equivalent assurance to an entirely hand-written proof. This technique forms the basis of a scalable approach to formal verification of large software systems.


http://fm2015.ifi.uio.no/


nicta:8497


Fernandez, Matthew; Andronick, June; Klein, Gerwin; Kuz, Ihor. Automated Verification of RPC Stub Code. In: International Symposium on Formal Methods; Oslo, Norway. 2015-06-20. 273-290.



Loading citation data...

Citation counts
(Requires subscription to view)