Awesome
Sys: A Static/Symbolic Tool for Finding Good Bugs in Good (Browser) Code
If you're interested, check out the (very very very) new reimplementation over here!
Install
Install dependencies
If you want to install Sys locally:
- llvm-9, llvm-9-tools
- boolector configured with
--shared
option. See thebuild()
andpackage()
functions in this file as an example of how to install boolector after you clone it. On Arch Linux, you can just installboolector-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
filesO0
matches all*.ll-O0
and*.ll-O0_p
filesO1
matches all*.ll-O1
and*.ll-O1_p
filesO2
matches all*.ll-O2
and*.ll-O2_p
filesO3
matches all*.ll-O3
and*.ll-O3_p
filesOg
matches all*.ll-Og
and*.ll-Og_p
filesOs
matches all*.ll-Os
and*.ll-Os_p
filesOz
matches all*.ll-Oz
and*.ll-Os_z
filesprod
matches all*_p
filesany
matches all files
- The
-c
option is used to specify the checker to run, one of:uninit
: Uninitialized memory checkerheapoob
: Malloc OOB checkerconcroob
: Negative index OOB checkeruserinput
: 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