This repository contains the code for SAWScript, the scripting language that forms the primary user interface to the Software Analysis Workbench (SAW). It provides the ability to reason about formal models describing the denotation of programs written in languages such as C, Java, and Cryptol.
Precompiled SAWScript binaries for a variety of platforms are available on the releases page.
SAW can use many theorem provers, but because of its use of Cryptol it always needs to have Microsoft Research's Z3 SMT solver installed. You can download Z3 binaries for a variety of platforms from their releases page.
We currently recommend Z3 4.8.7. If you plan to use path satisfiability checking, you'll also need Yices version 2.6.1 or newer.
After installation, make sure that
z3.exe on Windows)
is on your PATH.
To build SAWScript and related utilities from source:
Ensure that you have the
ghcexecutables in your
PATH. If you don't already have them, we recommend using
ghcupto install them: https://www.haskell.org/ghcup/
Ensure that you have the C libraries and header files for
terminfo, which generally comes as part of
ncurseson most platforms. On Fedora, it is part of the
ncurses-compat-libspackage. You will also need the C headers for
Ensure that you have the programs
PATH. Z3 binaries are available at https://github.com/Z3Prover/z3/releases
Optionally, put in place dependency version freeze files:
ln -s cabal.<ghc version>.config cabal.project.freeze
Build SAWScript by running
The SAWScript executables will be available in the
Optionally, run ./stage.sh to create a binary tarball.
Notes on LLVM
SAW can analyze LLVM programs (usually derived from C, but potentially
for other languages). The only tool strictly required for this is a
compiler that can generate LLVM bitcode, such as
having the full LLVM tool suite available can be useful. We have tested
SAW with LLVM and
clang versions from 3.5 to 9.0, as well as the
clang bundled with Apple Xcode. We welcome bug reports on
any failure to parse bitcode from LLVM versions in that range.
Note that successful parsing doesn't necessarily mean that verification
will be possible for all language constructs. There are various
instructions that are not supported during verification. However,
any failure during
llvm_load_module should be considered a bug.
Many dependencies are automatically downloaded into
deps/ when you
Manual Installation above. Key automatically
downloaded dependencies include:
deps/abcBridge/: Haskell bindings for ABC
deps/crucible/: Crucible symbolic execution engine
deps/jvm-verifier/: Java Symbolic Simulator (JSS)
deps/saw-core/: SAWCore intermediate language, used by CSS, JSS, and SAWScript
For SAW developers
saw-script main executable cannot be loaded into GHCi due to a
linker issue. However, the rest of the library can be manipulated in GHCi, with
a little convincing.
If you are using
cabal to build, select the
$ cabal new-repl saw-script
In order to use interactive tools like
intero, you need to configure them with
this target. You can configure
intero-mode in Emacs to use the
library target by setting the variable
intero-targets to the string
"saw-script:lib". To make this setting persistent for all files in this
project, place the following snippet in the file
((haskell-mode (intero-targets "saw-script:lib")))
Much of the work on SAW has been funded by, and lots of design input was provided by the team at the NSA's Laboratory for Advanced Cybersecurity Research, including Brad Martin, Frank Taylor, and Sean Weaver.
Portions of SAW are also based upon work supported by the Office of Naval Research under Contract No. N68335-17-C-0452. Any opinions, findings and conclusions or recommendations expressed in this material are those of the author(s) and do not necessarily reflect the views of the Office of Naval Research.