Use-case highlights and awards

STP has been used in over 100 research and industrial projects and has won numerous awards. Below is a non-exhaustive list of these awards and use-cases

Awards

Bug Finding and Symbolic Execution Tools

  • KLEE symbolic fuzzer is using STP at its core (Professor Cristian Cadar's group at Imperial College, London, and Professor Dawson Engler's group at Stanford University)
  • Souper project at the University of Utah and Google
  • S2E at EPFL
  • Mayhem fuzzer, which found over 1000 bugs in mainline Debian is using KLEE and hence STP.
  • Binary Analysis Platform (BAP) is using STP for analysis, by the CMU
  • EXE is a symbolic-execution based bug-finding tool that reads your C program and tries to automatically crash it (Stanford University)
  • MINESWEEPER  is a tool that automatically analyzes certain malicious behavior in unix utilities and malware.  (Carnegie Mellon University)
  • CATCHCONV is a bug finding tool that tries to find bugs due to type mismatch in C programs. (University of California, Berkeley)
  • Backward path-sensitive analysis of C programs to find bugs by Tim Leek from MIT Lincoln Labs
  • Bug finding in Verilog code (a major microprocessor company)
  • JPF-SE is a symbolic execution extension to the Java PathFinder model checker . (NASA Ames Research Center)
  • Avalanche bug-finding tool (Institute of Systems Programming, Moscow, Russia)
  • Low-level Bounded Model Checker - LLBMC   (Karlsruhe Institute of Technology (KIT), Germany)
  • FuzzGrind  (ESEC Lab)
  • Smart fuzzing prototype for the automatic detection of security vulnerabilities in executable code
  • The BlueSpec Hardware/Software Compiler company is using STP at its primary backend SMT solver (source of information: Dr. Nirav Dave of SRI International and MIT)

Formal Verification Tools

  • In conjunction with ACL2 to formally verify implementation of encryption algorithms in Java (Stanford University)
  • Formal verification of Parallel Transaction Architecture (Stanford University)

Other security vulnerability checkers

  • REPLAYER is a tool that replays an application dialog between two hosts in order to analyze security exploits (Carnegie Mellon University)
  • Hampi : A solver for string constraints used to automatically construct SQL injection and XSS exploits (MIT)
  • Used at Akamai to find security errors in infra-critical software

Other significant projects

  • Prophet for development and deployment of distributed systems (EPFL, Switzerland)
  • Automatic configuration: Tvl2STP (University of Namur in Belgium)
Comments