Conference item

Towards automated bounded model checking of API implementations

Abstract:: We introduce and demonstrate the viability of a novel technique for verifying that implementations of application program interfaces (APIs) are bug free. Our technique applies a new abstract interpretation to extract an underlying model of API usage, and then uses this to synthesise a set of verifiable program fragments. These fragments are evaluated using CBMC and any potentially spurious property violation is presented to a domain expert user. The user’s response is then used to refine the underlying model of the API to eliminate false positives. The refinement-analysis process is repeated iteratively. We demonstrate the viability of the technique by showing how it can find an integer underflow within Google’s Brotli, an underflow that has been shown to lead directly to allow remote attackers to execute arbitrary code in CVE 2016-1968.

Publication status:: Published

Peer review status:: Peer reviewed

Actions

Email

Email this record

Send the bibliographic details of this record to your email address.

Your Email
Please enter the email address that the record information will be sent to.

-
Your message (optional)
Please add any additional information to be included within the email.
Share
Cite

Cite this record

APA Style

Neville, D., Malton, A., Brain, M., & Kroening, D. (2016). Towards automated bounded model checking of API implementations. 1639, 31–42.

MLA Style

Neville, D, et al. “Towards Automated Bounded Model Checking of API Implementations.” vol. 1639, 2016, pp. 31–42.

Chicago Style

Neville, D, A Malton, M Brain, and D Kroening. 2016. “Towards Automated Bounded Model Checking of API Implementations.” 1639: 31–42.
Print

Access Document

Files:: Kroening et al, Towards automated bounded model checking of AP...

(Preview, Accepted manuscript, pdf, 402.5KB, Terms of use)

Authors

+ Neville, D More by this author

Institution:: University of Oxford
Oxford college:: St Anne's College
Role:: Author

+ Malton, A More by this author

Role:: Author

+ Brain, M More by this author

Institution:: University of Oxford
Division:: MPLS
Department:: Computer Science
Role:: Author

+ Kroening, D More by this author

Institution:: University of Oxford
Division:: MPLS
Department:: Computer Science
Role:: Author

Publisher:: CEUR-WS
Host title:: CEUR Workshop Proceedings
Journal:: CEUR Workshop Proceedings More from this journal
Volume:: 1639
Pages:: 31-42
Publication date:: 2016-07-01
Acceptance date:: 2016-04-19
ISSN:: 1613-0073

Pubs id:: pubs:641256
UUID:: uuid:9f95a39a-0a4a-42c6-acdc-696a07061375
Local pid:: pubs:641256
Source identifiers:: 641256
Deposit date:: 2017-01-28
ARK identifier:: ark:/29072/ora_9f95a39a0a4a42c6acdc696a07061375

Terms of use

Copyright holder:: Kroening et al
Copyright date:: 2016
Notes:: Copyright © 2016 for the individual papers by the papers' authors. Copying permitted for private and academic purposes. This volume is published and copyrighted by its editors.

Licence:: Terms and Conditions of Use for Oxford University Research Archive

Views and Downloads

About views and downloads

If you are the owner of this record, you can report an update to it here: Report update to this record

TO TOP