New Features
SAW can now use the ABC prover as an external process in addition to the linked-in version. This change is in preparation for removing the linked-in version in a future release. This change has several parts:
- The new proof tactics
w4_abc_verilog
andw4_abc_smtlib2
allow using ABC to discharge proof goals using either Verilog or SMT-Lib2 as the intermediate file format, respectively. - The new
offline_verilog
tactic writes a proof goal in the subset of Verilog supported by ABC, which can allow the use of custom ABC commands to discharge it. - The new
w4_offline_smtlib2
writes a proof goal in SMT-Lib2 syntax using What4 instead of SBV. - The new
write_verilog
command will write aTerm
to a file in Verilog syntax from the top level of a script. - The new
write_smtlib2_w4
command will write aTerm
to a file in SMT-Lib2 syntax from the top level of a script, using What4 instead of SBV. - The new proof tactics
sbv_abc
,sbv_boolector
,sbv_cvc4
,sbv_mathsat
,sbv_yices
,sbv_z3
,sbv_unint_cvc4
,sbv_unint_yices
, andsbv_unint_z3
are now aliases for the same tactics without thesbv_
prefixes in preparation for making the unprefixed tactics refer to the What4 versions of the same functionality.
Java verification using the Crucible symbolic execution engine is now more flexible and performant.
- The new
jvm_array_is
command specifies the entire contents of an array together. - The new
jvm_field_is
command allows disambiguation by type for fields of the same name but different types. - JVM method names can be disambiguated using type descriptors.
- JVM constructors can be referred to by the name
<init>
. - Error messages in JVM verification are significantly more helpful.
These changes, and various internal performance improvements, mean that the ECDSA verification example included with SAW now runs in around 5 minutes on a modern laptop.
New features exist to summarize any verifications performed with SAW. The summarize_verification
command will print a list of all functions or methods verified or assumed, and all lemmas proved with commands such as prove
. These summaries include the status (verified or assumed) of each item along with the provers used to complete the proof. The -s <filename>
flag will instruct SAW to automatically write a summary to the given file, and the -f <format>
flag will instruct SAW to use either a human-readable (pretty
) format or JSON (json
) for consumption by other tools.
An experimental RPC server for SAW now exists, which provides an alternative to SAWScript for controlling SAW execution. A client library for interacting with the server from Python exists here.
Verification of x86 code called from LLVM is now more flexible. The add_x86_preserved_reg
command can add a specific register to the set that is assumed to be callee-saved, and path satisfiability checking is now performed when passing True
as the fifth argument to crucible_llvm_verify_x86
.
The new cryptol_add_path
command adds a directory to the search path used when loading Cryptol modules (and following imports within explicitly-loaded modules).
New, shorter names are available for all LLVM commands starting with the crucible_
prefix. The new names use the llvm_
prefix instead. The top-level function crucible_llvm_verify
is now llvm_verify
, and crucible_llvm_unsafe_assume_spec
is llvm_unsafe_assume_spec
. The old names are still supported for now. The in-REPL documentation (:? <command>
) gives the new name for each command.
Shorter names are available for some saw-script types: CrucibleSetup
is now LLVMSetup
, CrucibleMethodSpec
is now simply LLVMSpec
, and JVMMethodSpec
is JVMSpec
. The old type names are still supported for backward compatibility.
Bug Fixes
-
Catch more exceptions at the REPL (issues #138, #560, #745, and #814).
-
Ensure global memory is immutable in x86 verification.
-
Closed issues #61, #138, #158, #162, #212, #215, #265, #314, #319, #399, #412, #422, #439, #456, #544, #560, #562, #683, #686, #719, #723, #745, #814, #844, #845, #856, #866, #874, #888, #901, #902, #904, #911, #920, #936, #937, #945, and #957.
Assets
6
github-actions
released this
New Features
-
Added experimental support for compositional extraction. Previously,
crucible_llvm_extract
and similar functions could translate very simple imperative functions intoTerm
models but analysis of more complex programs typically required verification of equivalence to Cryptol specifications. Now, thecrucible_llvm_compositional_extract
function allows extraction of any function that can be specified using aCrucibleSetup
block of the sort used forcrucible_llvm_verify
. In addition, this extraction can be compositional, preserving the call structure that exists in the original program instead of inlining everything. -
Added experimental support for interactive offline proofs using Coq. The
write_coq_term
function andoffline_coq
tactic will export the associatedTerm
to a file in Gallina syntax. This file can be imported into a Coq file that can do arbitrarily complex interactive proofs. -
Added experimental support for arrays of symbolic size. The new
crucible_array_alloc
function specifies the existence of an allocated array where the size is given by itsTerm
argument. The newcrucible_points_to_array_prefix
function specifies that the given pointer points to (the prefix of) a symbolic array value of a given symbolic size. -
Improved x86 verification capabilities. Verification scripts for x86 functions can now process functions with mutable globals and function calls (which are currently inlined), and can use proof scripts to discharge proof obligations.
-
Added a new
llvm_sizeof
primitive, which works similarly to thesizeof
operator in C. -
Added support for the
llvm.fshl.i32
funnel shift intrinsic. -
Added experimental support for verification summaries. These summaries list all verifications performed within a script in a concise way that can track arbitrarily complex proof orchestrations. Future releases will include more information in these summaries, and more textual explanation of the assumptions made during each proof.
Other Changes
-
Made small improvements to documentation and error messages throughout.
-
Improved the performance of expression hashing (closing #674).
-
Updated to include Cryptol 2.9.1 and all the associated changes.
Bug Fixes
-
Fixed handling of jumps in x86 verification.
-
Fixed matching for points-to and return values for x86.
-
Closed issues #140, #195, #225, #226, #387, #538, #542, #543, #556, #635, #640, #642, #674, #691, #693, #698, #699, #700, #701, #702, #704, #706, #707, #709, #720, #721, #730, #742, #744, #763, #768, #773, #783, #785, #789, #782, #803, #807, and #815.
Assets
6
New Features
-
Added experimental support for basic, non-compositional verification
of x86 machine code for use in conjunction with LLVM verification.crucible_llvm_verify_x86 : LLVMModule -> String -> String -> [(String, Int)] -> Bool -> CrucibleSetup () -> TopLevel CrucibleMethodSpec
The first argument specifies the LLVM module containing the caller.
The second and third specify the ELF file name and symbol name of the
function to be verifier. The fourth specifies the names and sizes (in
bytes) of global variables to initialize, and the fifth whether to
perform path satisfiability checking. The last argument is the LLVM
specification of the calling context against which to verify the
function. -
Added support for using the SMT theory of arrays in the LLVM memory
model. In some cases, this can significantly improve performance.enable_smt_array_memory_model : TopLevel () disable_smt_array_memory_model : TopLevel ()
-
Added support for specifying alignment in LLVM allocations. The
crucible_alloc_aligned
andcrucible_alloc_readonly_aligned
functions allocate read-write and read-only memory regions,
respectively, with the specified alignment (in bytes). -
Added a conditional points-to function,
crucible_conditional_points_to
, that allows an LLVM function to
conditionally modify memory, leaving it in its previous state
(potentially uninitialized) when the condition is false. -
Added several new options:
-
New functions
enable_what4_hash_consing
and
disable_what4_hash_consing
to enable or disable hash consing to
increase sub-formula sharing during symbolic execution. -
New functions
enable_crucible_assert_then_assume
and
disable_crucible_assert_then_assume
to control whether
predicates are assumed after asserting them during symbolic
execution. The default is now to not assume them, whereas
previously they were assumed. -
New command-line option
--no-color
to print an ASCII logo
without ANSI color or Unicode.
-
Performance Improvements
-
Improved performance of the LLVM memory model.
-
Improved performance of bitvector operations during symbolic execution.
-
Improved performance of rewriting SAWCore terms.
Bug Fixes
-
Fixed SBV interface to fail more gracefully when it cannot find the
solver executable. -
Fixed SMT-Lib export negation issues.
Fixes issues #286, #489, #491, #564, #580, #583, #585, #586, #587, #590,
#592, #594, #597, #598, #602, #603, #612, #613, #622, #626, #633, #638,
#639, and #647.
Assets
8
-
Fixed a long-standing soundness issue (#30) in compositional verification of LLVM programs. Previously, a specification for a function that neglected to mention an effect that the function in fact caused could be successfully verified. When verifying a caller of that function, only the effects mentioned in the specification would be used. The fix for this issue may break some proof scripts: any pointer mentioned using
crucible_points_to
in the initial state of a specification but not in the final state will be assigned a final value of "invalid", and any subsequent reads from the pointer will fail. To fix this issue, make sure that every specification you use provides a final value for every pointer it touches (which in many cases will be the same as its initial value). -
Added an experimental command,
llvm_boilerplate
, that emits skeleton function specifications for every function defined in an LLVM module. The additionalcrucible_llvm_array_size_profile
command can be used to refine the results ofllvm_boilerplate
based on the array sizes used by calls that arise from a call to the named top-level function. -
Added support for using the symbolic execution profiler available in Crucible. The
enable_crucible_profiling
command causes profiling information to be written to the given directory. This can then be visualized using the rendering code available here. -
Added proof tactics to use Yices (
w4_unint_yices
) and CVC4 (w4_unint_cvc4
) through the What4 backend instead of SBV. -
Modified the messages emitted for failed points-to assertions to be in terms of LLVM values.
-
Added support for using the SMT array memory model to reason about the LLVM heap. The
enable_smt_array_memory_model
command enables it for all future proofs. -
LLVM bitcode format support is improved. Versions 3.5 to 9.0 are known to be mostly well-supported. We consider parsing failures with any version newer than 3.5 to be a bug, so please report them on GitHub.
-
New experimental model counting commands
sharpSAT
andapproxmc
bind to the external tools of the same name. These were mistakenly listed as included in 0.3. -
Built against Cryptol 2.8.0.
-
Improved error messages in general.
-
Fixed various additional bugs, including #211, #455, #479, #484, #493, #496, #511, #521, #522, #534, #563
Assets
8
-
Java and LLVM verification has been overhauled to use the new Crucible symbolic execution engine. Highlights include:
-
New
crucible_llvm_verify
andcrucible_llvm_extract
commands replacellvm_verify
andllvm_extract
, with a different structure for specification blocks. -
LLVM verification tracks undefined behavior more carefully and has a more sophisicated memory model. See the manual for more.
-
New, experimental
crucible_jvm_verify
andcrucible_java_extract
commands will eventually replacejava_verify
andjava_extract
. For the moment, the former two are enabled with theenable_experimental
command and the latter two are enabled withenable_deprecated
. -
More flexible specification language allows convenient description of functions that allocate memory, return arbitrary values, expect explicit aliasing, work with NULL pointers, cast between pointers and integers, or work with opaque pointers.
-
Ghost state is supported in LLVM verification, allowing reasoning about certain complex or unavailable code.
-
Verification of LLVM works for a larger subset of the language, which particularly improves support for C++.
-
-
LLVM bitcode format support is greatly improved. Versions 3.5 to 7.0 are known to be mostly well-supported. We consider parsing failures with any version newer than 3.5 to be a bug, so please report them on GitHub.
-
Greatly improved error messages throughout.
-
Built against Cryptol 2.7.0.
-
New model counting commands
sharpSAT
andapproxmc
bind to the external tools of the same name. -
New proof script commands allow multiple goals and related proof tactics. See the manual.
-
Can be built with Docker, and will be available on DockerHub.
-
Includes an Emacs mode.
Assets
8
- Released under the 3-clause BSD license
- Major improvements to the Java and LLVM verification infrastructure,
as described in more detail here:- Major refactoring and polish to
java_verify
andjava_symexec
- Major refactoring and polish to
llvm_verify
andllvm_symexec
- Fixed soundness bug in
llvm_verify
treatment of heap
modifications - Fixed soundness bug related to
java_assert
andllvm_assert
- Support for branch satisfiability checking to be configured
- Support for some types of allocation in
java_verify
, enabled
withjava_allow_alloc
- Improved support for LLVM structs (including the
llvm_struct
type forllvm_verify
) - Support for non-scalar return values in
java_verify
and
java_symexec
- Support for using
java_ensure_eq
on fields of return value - Access to safety conditions in
java_symexec
andllvm_symexec
- New primitives
llvm_assert_eq
andjava_assert_eq
- Major refactoring and polish to
- Some changes to the SAWScript language:
- Conditional expressions including the keywords
if
,then
, and
else
, and the new constantstrue
andfalse
- New
eval_int
andeval_bool
functions to expose Cryptol bit
vectors andBit
values asInt
andBool
values in SAWScript - Pattern matching for tuples
- Improvements to pretty printing, including:
set_base
and
set_ascii
commands to control the formatting of values; ashow
function to convert a value to a string without printing it; and
the ability to useprint
orshow
instead of
llvm_browse_module
andjava_browse_class
- New built-in functions for processing lists
- Conditional expressions including the keywords
- New proof backends:
- A new
rme
proof tactic, based on the
Reed-Muller Expansion
normal form for propositional formulas. This tactic is
particularly efficient for dealing with polynomials over Galois
fields, as used in AES, for instance.
- A new
- Linked against the latest Cryptol code, which includes the following
changes since release 2.3.0:- An extended prelude with more Haskell-like functions
- Better, more portable seeding for
random
- Performance improvements for symbolically executing tables of
constant values - Performance improvements for type checking large constants
- Internal improvements:
- Simplified Cryptol to SAWCore translation
- Improved performance of Cryptol to SAWCore translation for
recursive functions - Updated bitcode parser to support some of the changes in LLVM 3.7
- Many bug fixes
- Many code cleanups
Assets
12
Release of version 0.1-dev