All Projects → PLSysSec → Sys

PLSysSec / Sys

Licence: gpl-2.0
Sys: A Static/Symbolic Tool for Finding Good Bugs in Good (Browser) Code

Projects that are alternatives of or similar to Sys

Crab Llvm
Static Analyzer for LLVM bitcode based on Abstract Interpretation
Stars: ✭ 143 (-4.03%)
Mutual labels:  static-analysis, llvm
Crosshair
An analysis tool for Python that blurs the line between testing and type systems.
Stars: ✭ 586 (+293.29%)
Mutual labels:  static-analysis, symbolic-execution
Phasar
A LLVM-based static analysis framework.
Stars: ✭ 503 (+237.58%)
Mutual labels:  static-analysis, llvm
Seahorn
SeaHorn Verification Framework
Stars: ✭ 270 (+81.21%)
Mutual labels:  static-analysis, llvm
Cxxctp
DEPRECATED. USE INSTEAD github.com/blockspacer/flextool
Stars: ✭ 58 (-61.07%)
Mutual labels:  static-analysis, llvm
Clang Power Tools
Bringing clang-tidy magic to Visual Studio C++ developers.
Stars: ✭ 285 (+91.28%)
Mutual labels:  static-analysis, llvm
Tigress protection
Playing with the Tigress binary protection. Break some of its protections and solve some of its challenges. Automatic deobfuscation using symbolic execution, taint analysis and LLVM.
Stars: ✭ 550 (+269.13%)
Mutual labels:  llvm, symbolic-execution
clam
Static Analyzer for LLVM bitcode based on Abstract Interpretation
Stars: ✭ 180 (+20.81%)
Mutual labels:  llvm, static-analysis
Apisan
APISan: Sanitizing API Usages through Semantic Cross-Checking
Stars: ✭ 46 (-69.13%)
Mutual labels:  static-analysis, symbolic-execution
Stoat
STatic (LLVM) Object file Analysis Tool
Stars: ✭ 44 (-70.47%)
Mutual labels:  static-analysis, llvm
crusher
No description or website provided.
Stars: ✭ 21 (-85.91%)
Mutual labels:  static-analysis, symbolic-execution
Sea Dsa
A new context, field, and array-sensitive heap analysis for LLVM bitcode based on DSA.
Stars: ✭ 90 (-39.6%)
Mutual labels:  static-analysis, llvm
progge.rs
Program analysis playground for a simple, imperative language
Stars: ✭ 29 (-80.54%)
Mutual labels:  llvm, static-analysis
Clangkit
ClangKit provides an Objective-C frontend to LibClang. Source tokenization, diagnostics and fix-its are actually implemented.
Stars: ✭ 330 (+121.48%)
Mutual labels:  static-analysis, llvm
SixtyPical
A 6502-oriented low-level programming language supporting advanced static analysis
Stars: ✭ 25 (-83.22%)
Mutual labels:  static-analysis, symbolic-execution
Svf
Static Value-Flow Analysis Framework for Source Code
Stars: ✭ 540 (+262.42%)
Mutual labels:  static-analysis, llvm
CFI-LB
Adaptive Callsite-sensitive Control Flow Integrity - EuroS&P'19
Stars: ✭ 13 (-91.28%)
Mutual labels:  llvm, symbolic-execution
surveyor
A symbolic debugger for C/C++ (via LLVM), machine code, and JVM programs
Stars: ✭ 14 (-90.6%)
Mutual labels:  llvm, symbolic-execution
Domtresat
Dominator Tree LLVM Pass to Test Satisfiability
Stars: ✭ 42 (-71.81%)
Mutual labels:  static-analysis, llvm
Codechecker
CodeChecker is an analyzer tooling, defect database and viewer extension for the Clang Static Analyzer and Clang Tidy
Stars: ✭ 1,209 (+711.41%)
Mutual labels:  static-analysis, llvm

Sys: A Static/Symbolic Tool for Finding Good Bugs in Good (Browser) Code

Install

Install dependencies

If you want to install Sys locally:

  • llvm-9, llvm-9-tools
  • boolector configured with --shared option. See the build() and package() functions in this file as an example of how to install boolector after you clone it. On Arch Linux, you can just install boolector-git from AUR.
  • The Haskell tool Stack

Alternatively, you can use the Dockerfile from Ralf-Philipp Weinmann.

Build project

Once you have all the dependencies installed you should be able to just build the tool:

stack build

Test

Once you built the tool you can build and run our tests with:

stack test

This will run a more-or-less full version of our test suite, along with regression tests for every bug that we list in the paper. The suite takes a little over two minutes on laptop with 64GB of RAM and 8 threads. All tests with one exception---a bug whose source we're having trouble tracking down---should pass. If anything else fails, try re-running the tests; the solver may have timed out (this hasn't happened on our machines, but since we can't give you a login for annonymity, its a possibility that it will happen on your machine).

If you just want to reproduce the paper results and nothing else, run:

stack test --ta '-p End-to-end'

Run

Once you built the tool you can now use it to find bugs!

stack exec sys

The tool takes several options:

  -d DIR    --libdir=DIR   directory (or file) to analyze
  -e EXTN   --extn=EXTN    file extension
  -c CHECK  --check=CHECK  checker to run
  • The -d option is used to specify the directory (containing the LLVM files) or a single LLVM file.
  • The -e option is used to specify the extension of files to check. This is useful when building your project with different optimizations levels (e.g., .ll-O0 for debug build with -O0 and .ll-O0_p for production).
    • ll matches all *.ll files
    • O0 matches all *.ll-O0 and *.ll-O0_p files
    • O1 matches all *.ll-O1 and *.ll-O1_p files
    • O2 matches all *.ll-O2 and *.ll-O2_p files
    • O3 matches all *.ll-O3 and *.ll-O3_p files
    • Og matches all *.ll-Og and *.ll-Og_p files
    • Os matches all *.ll-Os and *.ll-Os_p files
    • Oz matches all *.ll-Oz and *.ll-Os_z files
    • prod matches all *_p files
    • any matches all files
  • The -c option is used to specify the checker to run, one of:
    • uninit: Uninitialized memory checker
    • heapoob: Malloc OOB checker
    • concroob: Negative index OOB checker
    • userinput: User input checker

Example

To find the uninitialized memory access bug that our tool found in Firefox's Prio library:

$ stack exec sys -- -c uninit -e prod -d ./test/Bugs/Uninit/Firefox/serial.ll-O2_p

The tool flags two bugs. Let's look at the first:

Stack uninit bug
Name "serial_read_mp_array_73"
in 
Name "serial_read_mp_array"
path-to-file
[UnName 4,UnName 71]

If you inspect the serial_read_mp_array() function, the buggy block path is %4 (the first block) to %71,where we use [%73].

Help

We haven't tested (and likely won't test) Sys on anything but Arch Linux. We're happy to integrate patches that add support for other OSes and build systems though!

Directory structure

├── app            -- Executable used to run the checkers
├── src
│   ├── Checkers   -- Static and symbolic checkers
│   ├── Control    -- Logging helpers
│   ├── LLVMAST    -- LLVM AST interface
│   ├── InternalIR -- Internal IR used to represent paths for both static and symex
│   ├── Static     -- Static checker DSL
│   └── Symex      -- Symbolic DSL and execution engine
├── community      -- Community files
└── test           -- Tests
Note that the project description data, including the texts, logos, images, and/or trademarks, for each open source project belongs to its rightful owner. If you wish to add or remove any projects, please contact us at [email protected].