Sys: A Static/Symbolic Tool for Finding Good Bugs in Good (Browser) Code
If you want to install Sys locally:
- llvm-9, llvm-9-tools
- boolector configured with
--sharedoption. See the
package()functions in this file as an example of how to install boolector after you clone it. On Arch Linux, you can just install
- The Haskell tool Stack
Alternatively, you can use the Dockerfile from Ralf-Philipp Weinmann.
Once you have all the dependencies installed you should be able to just build the tool:
Once you built the tool you can build and run our tests with:
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'
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
-doption is used to specify the directory (containing the LLVM files) or a single LLVM file.
-eoption is used to specify the extension of files to check. This is useful when building your project with different optimizations levels (e.g.,
.ll-O0for debug build with
anymatches all files
-coption 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
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 [
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!
├── 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