Trustworthy Systems

Automated verification of RPC stub code

Authors

Matthew Fernandez, June Andronick, Gerwin Klein and Ihor Kuz

NICTA

UNSW

Abstract

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.

BibTeX Entry

  @inproceedings{Fernandez_AKK_15,
    address          = {Oslo, Norway},
    author           = {Fernandez, Matthew and Andronick, June and Klein, Gerwin and Kuz, Ihor},
    booktitle        = {International Symposium on Formal Methods (FM)},
    month            = jun,
    pages            = {273--290},
    paperurl         = {https://trustworthy.systems/publications/nicta_full_text/8497.pdf},
    slides           = {https://trustworthy.systems/publications/nicta_slides/8497.pdf},
    title            = {Automated Verification of {RPC} Stub Code},
    year             = {2015}
  }

Download