Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Adaptive Exploit Generation against Security Devices and Security APIs

Robert Künnemann, Julian Biehl

TL;DR

This work shows how to automatically derive proof-of-concept exploits against Security APIs using formal methods, and extends the popular protocol verifier ProVerif with a language-agnostic template mechanism that can transform attack traces into programs.

Abstract

Proof-of-concept exploits help demonstrate software vulnerability beyond doubt and communicate attacks to non-experts. But exploits can be configuration-specific, for example when in Security APIs, where keys are set up specifically for the application and enterprise the API serves. In this work, we show how to automatically derive proof-of-concept exploits against Security APIs using formal methods. We extend the popular protocol verifier ProVerif with a language-agnostic template mechanism. Employing program snippets attached to steps in the model, we can transform attack traces (which ProVerif typically finds automatically) into programs. Our method is general, flexible and convenient. We demonstrate its use for the W3C Web Cryptography API, for PKCS#11 and for the YubiHSM2, providing the first formal model of the latter.

Adaptive Exploit Generation against Security Devices and Security APIs

TL;DR

This work shows how to automatically derive proof-of-concept exploits against Security APIs using formal methods, and extends the popular protocol verifier ProVerif with a language-agnostic template mechanism that can transform attack traces into programs.

Abstract

Proof-of-concept exploits help demonstrate software vulnerability beyond doubt and communicate attacks to non-experts. But exploits can be configuration-specific, for example when in Security APIs, where keys are set up specifically for the application and enterprise the API serves. In this work, we show how to automatically derive proof-of-concept exploits against Security APIs using formal methods. We extend the popular protocol verifier ProVerif with a language-agnostic template mechanism. Employing program snippets attached to steps in the model, we can transform attack traces (which ProVerif typically finds automatically) into programs. Our method is general, flexible and convenient. We demonstrate its use for the W3C Web Cryptography API, for PKCS#11 and for the YubiHSM2, providing the first formal model of the latter.
Paper Structure (34 sections, 6 equations, 1 figure, 3 tables)

This paper contains 34 sections, 6 equations, 1 figure, 3 tables.

Table of Contents

  1. Introduction
  2. PoC exploits: what is the use?
  3. PoCs are communication tools.
  4. PoC make analysis results accessible.
  5. PoCs are trivially sound.
  6. Related Work
  7. Security API analysis
  8. Attack recovery
  9. Preliminaries
  10. Term algebra
  11. Horn clauses
  12. Queries
  13. Running example
  14. ProVerif's resolution
  15. Approach
  16. ...and 19 more sections

Figures (1)

  • Figure 1: Example model.

Theorems & Definitions (15)

  • Example 1
  • Example 2
  • Definition 1: Subsumption BlanchetBook09
  • Definition 2: Derivability BlanchetBook09
  • Example 3
  • Definition 3
  • Definition 4: Horn clause substitution
  • Example 4
  • Definition 5: Function symbol annotation
  • Example 5
  • ...and 5 more