S2e

S2E

Built upon KLEE symbolic execution engine and the QEMU virtual machine.

Good:

  • works at any level of the stack: applications, libraries, kernel drivers, and device firmware.
  • generates test cases to prove the existence of vul;
  • Supports Windows & Linux: exe tracing, code coverage, profiling.
  • Explore thousands of paths automatically.

Modular/Extensible:

  • use its multi-path analysis (symbolic execution).
  • use as single-path instrumentation platform.
  • can be used without overhead of VM: S2E emulates KVM interfaces.

Program analysis capability:

  • navigate large state spaces with concolic and symbolic execution, state merging, static analysis, function summaries, incremental constraint solving.
  • Security checking, test, verification, reverse engineering, performance profiling, etc.
  • Quickly prototype your research ideas by combining existing plugins or writing your own.

Implementation:

Papers: 1 2 3 4 5 6

  1. Selective Symbolic Execution. Vitaly Chipounov, Vlad Georgescu, Cristian Zamfir, George Candea. 5th Workshop on Hot Topics in System Dependability (HotDep), Lisbon, Portugal, June 2009. ↩
  2. Reverse Engineering of Binary Device Drivers with RevNIC. Vitaly Chipounov and George Candea. 5th ACM SIGOPS/EuroSys European Conference on Computer Systems (EuroSys), Paris, France, April 2010. ↩
  3. Testing Closed-Source Binary Device Drivers with DDT. Volodymyr Kuznetsov, Vitaly Chipounov, George Candea. USENIX Annual Technical Conference (USENIX), Boston, MA, June 2010. DDT tool won the Silver Prize at the 2012 World Open-Source Software Challenge. ↩
  4. S2E: A Platform for In Vivo Multi-Path Analysis of Software Systems. Vitaly Chipounov, Volodymyr Kuznetsov, George Candea. 16th Intl. Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), Newport Beach, CA, March 2011. BEST PAPER AWARD. ↩
  5. Enabling Sophisticated Analysis of x86 Binaries with RevGen. Vitaly Chipounov and George Candea. 7th Workshop on Hot Topics in System Dependability (HotDep), Hong Kong, China, June 2011. ↩
  6. The S2E Platform: Design, Implementation, and Applications. Vitaly Chipounov, Volodymyr Kuznetsov, and George Candea. ACM Transactions on Computer Systems (TOCS) Special issue: Best papers of ASPLOS, February 2012. ↩
Created Nov 11, 2019 // Last Updated Nov 11, 2019

If you could revise
the fundmental principles of
computer system design
to improve security...

... what would you change?