Sireum: A Software Analysis Platform (v3)
Available Products
- Sireum Logika: A Program Verifier and a Natural Deduction Proof Checker for Propositional, Predicate, and Programming Logics
- Sireum Awas: An Information Flow Analyzer and Visualizer for Component-based Systems
Requirements for Running Sireum
Supported platforms (64-bit only):
-
macOS (test platform: 10.12 - 10.14)
-
Linux (test platform: Ubuntu 18.04)
-
Windows (test platform: Windows 10)
Installing and Running Sireum
Sireum v3 binary distributions that we provide are cryptographically-signed just in case you want to ensure that your copy is untampered read more.
The accompanying Minisign digital signature can be verified using the following command:
minisign -P RWShRZe/1tMRHAcQ2162Wq5FhU2ptktJdQxzUxvK0MwVjDYRC4JY87Fb -Vm <file>
Alternatively, you can use the following signify command:
signify -p sireum-v3-key.pub -x <file>.minisig -Vm <file>
where sireum-v3-key.pub
can be downloaded from: http://bit.ly/sv3key
Sireum Integrated Verification Environment (IVE)
Video Tutorial: Installing Sireum IVE in Windows
Sireum IVE includes a custom IntelliJ IDEA Community Edition with various plugins installed, along with the Sireum CLI (see below).
In addition to the regular Release builds, we also provide Development builds for trying out Sireum v3 experimental features.
-
macOS
Execute the following in a bash terminal:
(sim=sireum-v3-ive-mac64.dmg && rm -f $sim && curl -JLo $sim http://bit.ly/sv3ivem && open $sim)
Minisign: http://bit.ly/sv3ivems
Once it is done, it should open a new window:
Drag and drop the Sireum icon to the Applications folder.
(Note: the above avoids GateKeeper; if it is instead downloaded using a browser, you need to remove Apple's quarantine extended attribute on the .dmg file before opening it as follows:
xattr -d com.apple.quarantine sireum-v3-idea-mac64.dmg
).For subsequent instructions, replace
SIREUM_HOME
with/Applications/Sireum.app/Contents/Resources/sireum-v3
.To run Sireum IVE, double-click
Sireum
inside/Applications
(or, in a terminal:open /Applications/Sireum.app
).To run Sireum CLI in a terminal:
SIREUM_HOME/sireum
.Development Build:
(sdim=sireum-v3-dev-ive-mac64.dmg && rm -f $sdim && curl -JLo $sdim http://bit.ly/sv3divem && open $sdim)
Minisign: http://bit.ly/sv3divems
-
Linux
Download from: http://bit.ly/sv3ivel
Minisign: http://bit.ly/sv3ivels
Uncompress it in a folder whose path does not contain a whitespace such as
/opt
(or~/Applications
, if your home directory path does not contain a whitespace).For subsequent instructions, replace
SIREUM_HOME
with/opt/Sireum
(or~/Applications/Sireum
).To run Sireum IVE in a terminal:
SIREUM_HOME/idea
.To run Sireum CLI in a terminal:
SIREUM_HOME/sireum
.Development Build: http://bit.ly/sv3divel, Minisign: http://bit.ly/sv3divels
-
Windows
Download from: http://bit.ly/sv3ivew
Minisign: http://bit.ly/sv3ivews
Uncompress it to the
C:
drive root directory (i.e.,C:\
) so the fileC:\Sireum\sireum.bat
is present.For subsequent instructions, replace
SIREUM_HOME
withC:\Sireum
.To run Sireum IVE:
-
double-click, either:
-
32-bit:
SIREUM_HOME\apps\idea\bin\idea.exe
, or -
64-bit:
SIREUM_HOME\apps\idea\bin\idea64.exe
This requires Java 8 64-bit, which is available in
SIREUM_HOME\platform\java
; to use that, addSIREUM_HOME\platform\java\bin
to yourPATH
environment variable.
-
-
in a terminal:
SIREUM_HOME\idea.bat
orSIREUM_HOME\idea64.bat
.
To run Sireum CLI in a terminal:
SIREUM_HOME\sireum.bat
Development Build: http://bit.ly/sv3divew, Minisign: http://bit.ly/sv3divews
-
Sireum Command-Line Interface (CLI)
-
macOS
Download from: http://bit.ly/sv3clim
Minisign: http://bit.ly/sv3clims
Uncompress it in a folder whose path does not contain a whitespace such as
/opt
(or~/Applications
, if your home directory path does not contain a whitespace).For subsequent instructions, replace
SIREUM_HOME
with/opt/sireum-v3
(or~/Applications/sireum-v3
).To run Sireum CLI in a terminal:
SIREUM_HOME/sireum
.Development Build: http://bit.ly/sv3dclim, Minisign: http://bit.ly/sv3dclims
-
Linux
Download from: http://bit.ly/sv3clil
Minisign: http://bit.ly/sv3clils
Uncompress it in a folder whose path does not contain a whitespace such as
/opt
(or~/Applications
, if your home directory path does not contain a whitespace).For subsequent instructions, replace
SIREUM_HOME
with/opt/sireum-v3
(or~/Applications/sireum-v3
).To run Sireum CLI in a terminal:
SIREUM_HOME/sireum
.Development Build: http://bit.ly/sv3dclil, Minisign: http://bit.ly/sv3dclils
-
Windows
Download from: http://bit.ly/sv3cliw
Minisign: http://bit.ly/sv3cliws
Uncompress it to the
C:
drive root directory (i.e.,C:\
) so the fileC:\sireum-v3\sireum.bat
is present.For subsequent instructions, replace
SIREUM_HOME
withC:\sireum-v3
.To run Sireum CLI in a terminal:
SIREUM_HOME\sireum.bat
.Development Build: http://bit.ly/sv3dcliw, Minisign: http://bit.ly/sv3dcliws
Requirements for Buiding Sireum from Source
All Supported Platforms
- Required tools for building Sireum:
bash
,git
,unzip
,wget
,bc
Linux
- Required tools for building Sireum:
xz
Windows
-
Required tools for building Sireum: MSYS2
pacman -S git unzip wget bc
Installing and Running Sireum from Source
In a bash terminal:
-
Using HTTPS:
git clone --recursive https://github.com/sireum/v3.git sireum-v3 sireum-v3/sireum
-
Using SSH:
git clone --recursive git@github.com:sireum/v3.git sireum-v3 sireum-v3/sireum
(If this is your first time running the script, it first:
-
downloads Zulu JDK, Scala, Node.js and Sbt, and then installs them under the
platform
directory; -
downloads Z3 and installs it under the
apps
directory; and
Sireum: A Software Analysis Platform (v3)
(c) 2011-2017, SAnToS Laboratory, Kansas State University
http://sireum.org
Usage: sireum <mode>
Available mode(s):
logika Logika Program Verifier and Proof Checker
util Utility Tools
Updating
To get updates, simply do a git pull --recurse-submodules
inside sireum-v3
and run Sireum again:
cd sireum-v3
git pull --recurse-submodules
./sireum
Testing Sireum using Sbt
Run: sireum-v3/bin/sbt-launch.sh test
Building Sireum Distributions
Building Sireum CLI Distributions
Run: sireum-v3/distros/build.sh
The resulting bundles are located at: sireum-v3/distros
.
Building Sireum CLI and IVE Distributions
Requirements:
Run: sireum-v3/distros/build-idea.sh
The resulting bundles are located at: sireum-v3/distros
.
Docker Containers
Pre-Built Images
Pre-built container images are available at Docker Hub:
-
Sireum CLI: https://hub.docker.com/r/sireum/v3
docker run -it sireum/v3:latest /bin/bash
Sireum CLI is located at
/opt/sireum-v3/sireum
. -
Sireum CLI with CompCert (Non-Commercial Only): https://hub.docker.com/r/sireum/v3-compcert/
docker run -it sireum/v3-compcert:latest /bin/bash
Sireum CLI is located at
/opt/sireum-v3/sireum
.
Building Images
Run:
-
sireum-v3/docker/build.sh
The resulting image name is
sireum/v3:latest
. -
With CompCert (Non-Commercial Only):
sireum-v3/docker/build-compcert.sh
The resulting image name is
sireum/v3-compcert:latest
.
Issues?
Please file a new GitHub issue.
Assembling Sireum Jar
Run: sireum-v3/bin/sbt-launch.sh assembly
The jar will be located at sireum-v3/bin/sireum.jar
Development Environments
IntelliJ IDEA-based Sireum IVE described above (or standard IDEA Ultimate/Community Editions) are the recommended IDEs for Sireum v3 development.
CLion is recommended for C/C++ related development. JetBrains has graciously provided free licenses JetBrains' toolbox (including CLion) for Sireum project members.
Setting Up Sireum IVE for Sireum v3 Development
Note: If .idea
already exists, remove it first.
-
Retrieve Sireum IVE Development build (see above).
Increase memory settings for Sireum IVE in
<SIREUM-IVE-HOME>/.../bin/idea.vmoptions
or<SIREUM-IVE-HOME>/.../bin/idea64.vmoptions
. -
In Sireum IVE starting dialog window,
select "Import Project".
-
In the "Import Project" dialog window,
select "Import project from external model", select "SBT", and then click "Next".
-
Next,
set the "Project JDK" to "/Applications/Sireum.app/Contents/Resources/sireum-v3/platform/java".
Then, expand "Global SBT settings":
-
Max Heap Size
:4096
-
VM Parameters
:-XX:+UseG1GC -XX:ReservedCodeCacheSize=1G -Xss4m -Dorg.sireum.home=<SIREUM_HOME>
-
-
In the "SBT Project Data To Import" dialog,
all modules should have been selected by default; click "OK".