Sireum: A High Assurance System Engineering Platform

Overview

Sireum Kekinian is the most recent evolution of the Sireum platform whose core components are being built using the Sireum programming language -- Slang.

Slang is an OO/FP programming language with contract and proof languages designed for formal verification and analyses; that is, it serves as the basis for the next generation Logika verifier and proof checker, as well as for other formal method-based analysis techniques. It is currently a subset of Scala 2.13 with tailored semantics enabled via Scala's macro and compiler plugin facilities, supported with a customized version of IntelliJ -- Sireum IVE, and an accompanying build tool -- Proyek.

With the exception of a small part of its runtime library and its parser that uses scalameta, the runtime library and the Slang codebase itself (and analyses on top of it) are written using Slang.

Slang programs run on the JVM (Java 11+), in the browser or Node.js (via Scala.js Javascript translation), and natively via Graal targeting macOS, Linux, and Windows on amd64, and macOS and Linux on aarch64.

In addition, the Slang-to-C transpiler can compile a subset of Slang -- Slang Embedded (which excludes, e.g., closures and recursive types), to C99 without garbage-collection at runtime. The generated C code is both Slang source-traceable and in the form that is structurally close to the Slang source; in addition to gcc and clang, it can also be compiled using the CompCert Verified C Compiler to provide a high-assurance toolchain for program correctness down to machine code.

On all compilation targets (e.g., JVM, C, Javascript, etc.), Slang provides extension method facilities that can extend its language features and integrate with other programming languages, platform-specific libraries, and existing/legacy code.

Furthermore, Slang can also be used as a universal shell scripting language -- Slash, which can run on macOS, Linux, Windows, and others where a JVM runtime is available. Slash powers many of the shell scripts for developing Kekinian itself. As Slash is Slang, Slash scripts can be compiled to native via Graal, which speeds things up by virtue of having no JVM boot up time.

Available Products

• Slang: The Sireum Programming Language

  (ISoLA 2021: presentation, paper; simple examples)

• HAMR: Slang-based High Assurance Model-based Rapid Engineering of Embedded Systems

  (ISoLA 2021: presentation, paper)

• Logika: The Sireum Verification Framework

  (see it in action in the TCCoE 2022 presentation; the Logika predecessor pedagogical tool for teaching, along with its documentation and course notes, are available at: http://logika.v3.sireum.org)

• IVE: Slang IntelliJ-based Integrated Verification Environment

  (see it in action in the TCCoE 2022 presentation on Logika)

• Proyek: Incremental and Parallel Slang Build Tool

  (also suitable for Java and Scala/Scala.js projects; examples: simple, for Sireum itself)

• Parser Generator: LL(k), PEG/Packrat, or "mixed" (k-lookahead with backtracking) Slang parser generator

  It generates readable, easy-to-debug parser/lexer over Unicode codepoints in Slang, which can be compiled further to native or Javascript. The input grammar is a small subset of ANTLR3's grammar with IDE support. As an example, the parser generator uses its own generated parser/lexer to parse its input grammar to build general parse trees (that come with a generic tree rewriting algorithm for binary operators with configurable precedence/associativity rules after parsing).

• Presentasi: JavaFX Presentation Generator from Slang-based Specifications

  (including text-to-speech synthesizers; simple example, TCCoE 2022 presentation on Logika)

Installing

Sireum is available as pre-built binaries/installers or from source. The main advantage of using the source distribution is that updates can be done incrementally while the binary distribution requires complete re-installation. On the other hand, source distribution requires more setup. As Sireum is currently in its early active development phase, it is highly recommended to use the source distribution.

Additionally, it is included in a prebuilt case-env.ova Debian VM (which includes seL4, CompCert, OSATE, FMIDE, etc.; respective tool license terms apply).

Binary Distributions

The binary distribution files are available at: https://github.com/sireum/kekinian/releases

Sireum binary distribution files are 7z self-extracting archives (SFX) with command-line installers to (optionally) configure where Sireum should be installed (the files can also be extracted using a program capable of uncompressing 7z archive).

If you want to ensure that the downloaded files are genuine, download the appropriate Minisign signature file for the specific platform, then run:

minisign -P RWShRZe/1tMRHAcQ2162Wq5FhU2ptktJdQxzUxvK0MwVjDYRC4JY87Fb -VHm <installer-file>

Set the SIREUM_HOME env var to the Sireum installation path, then proceed to Using Sireum.

Git Source Distribution

Requirements:

• macOS: curl and git

• Linux (amd64, aarch64): curl and git

• Windows, either:

  • Using a NTFS partition with developer Mode enabled and git (Git For Windows, MSYS2, or Cygwin); or

  • WSL2 (Linux requirements apply)

Note that Sireum stores small, pre-built binary dependencies in its repositories. Virus analysis results are provided in the respective submodule repositories for macOS, Linux, and Windows.

Setup

In a console terminal:

• macOS/Linux:

  git clone --recursive https://github.com/sireum/kekinian
  kekinian/bin/build.cmd setup  # for non-POSIX shell, prefix with sh

• Windows:

  git clone --recursive https://github.com/sireum/kekinian
  kekinian\bin\build.cmd setup

The above install Sireum command-line interface (CLI) and its IntelliJ-based Integrated Verification Environment (IVE), as well as their dependencies. Set the SIREUM_HOME env var to the kekinian path above.

To update later on, simply do a git pull --recurse-submodules and re-run build.cmd setup (or simply build.cmd to rebuild Sireum CLI tools). Note that after a setup update, it is best to invalidate IntelliJ's cache files and restart by using IntelliJ's File -> Invalidate Caches... menu item and select Clear all file system cache and Local History.

Occasionally, there might be new API used in build.cmd that is available in the pre-built binary online but not in your local copy. This issue happens because build.cmd uses Sireum itself, hence it is a bootstraping issue. This issue typically manifests by build.cmd failing to compile/execute due to missing methods/classes. In that case, first delete your local sireum.jar in the bin directory and then re-run build.cmd setup.

If rebuilding Sireum somehow failed still, try cleaning the repo:

• macOS/Linux:

  ${SIREUM_HOME}/bin/clean.sh

• Windows:

  %SIREUM_HOME%\bin\clean.bat

The clean scripts remove all Sireum-related cache directories and revert any changes and delete new files in the local git repository.

After cleaning, re-run git pull --recurse-submodules (until it reaches a good fix-point) and build.cmd setup.

Remote Development Setup (Experimental)

Using JetBrains Projector

You can project Sireum IVE so it can be viewed by a web browser using JetBrains Projector that ships with IVE. To launch, click on "Projector" in the IVE status bar.

If you use Linux, you can launch Sireum IVE headless-ly by first installing the projector server:

$SIREUM_HOME/bin/install/projector-server.cmd
$SIREUM_HOME/bin/linux/idea/bin/projector-server.sh

Then open http://<machine-ip>:8887 in a browser.

Using JetBrains Gateway

IntelliJ Ultimate now supports remote development from a Linux server reachable using ssh, and Sireum IVE can be set up on top of it:

1. Use JetBrains Gateway to install an IntelliJ Ultimate instance in the Linux server.

   Note that the supported instance version of IntelliJ should be compatible with what is listed in version.properties with property key org.sireum.version.idea property key). If the listed property value is 20XX.Y.Z or 20XX.Y, then you need to IntelliJ Ultimate build that starts withXXY.

2. Connect to the server and install Sireum:

   git clone --recursive https://github.com/sireum/kekinian
   kekinian/bin/build.cmd setup-server
   

3. Open the kekinian path above with JetBrains Gateway/Client.

Using Vagrant and VirtualBox

By using Vagrant, you can automatically provision a VirtualBox Linux virtual machine (VM) with Sireum set up.

Please see the instructions at: https://github.com/sireum/case-env

Using Sireum

To launch the Sireum CLI or IVE:

• macOS:

  ${SIREUM_HOME}/bin/sireum                      # CLI
  open ${SIREUM_HOME}/bin/mac/idea/IVE.app       # IVE

• Linux (amd64):

  ${SIREUM_HOME}/bin/sireum
  ${SIREUM_HOME}/bin/linux/idea/bin/IVE.sh

• Linux (aarch64):

  ${SIREUM_HOME}/bin/sireum
  ${SIREUM_HOME}/bin/linux/arm/idea/bin/IVE.sh

• Windows:

  %SIREUM_HOME%\bin\sireum.bat
  %SIREUM_HOME%\bin\win\idea\bin\IVE.exe

To proceed, please read the quick tutorial at: https://github.com/sireum/proyek-example

Learning Slang by Examples

If you would like to learn Slang quickly, you can read and use Sireum IVE to experiment with several examples designed to highlight various Slang language features:

https://github.com/sireum/slang-by-examples

Sireum Development

Sireum is best developed (browsed/edited) by using Sireum IVE itself. The build.cmd setup command above setup IVE for Sireum development. If you want to re-run just the IVE project re-generation (e.g., when there are upgrades to some library dependencies), do the following in a terminal:

• macOS/Linux:

  ${SIREUM_HOME}/bin/build.cmd project

• Windows:

  %SIREUM_HOME%\bin\build.cmd project

Then open the SIREUM_HOME directory as a project in Sireum IVE.

To build Sireum assembly/CLI tool:

• macOS/Linux:

  ${SIREUM_HOME}/bin/build.cmd

• Windows:

   %SIREUM_HOME%\bin\build.cmd

Sireum Native Executable

It is recommended to compile Sireum (and Slash build scripts) to native as it removes JVM boot up time.

First, install GraalVM native-image's prerequisites (note: native-image for Windows requires Visual Studio Community 2017 or 2019); then, to build Sireum native executable:

• macOS/Linux:

  ${SIREUM_HOME}/bin/build.cmd native

• Windows:

  • Visual Studio 2022 Enterprise

    call "C:\Program Files\Microsoft Visual Studio\2022\Enterprise\VC\Auxiliary\Build\vcvars64.bat"
    %SIREUM_HOME%\bin\build.cmd native

  • Visual Studio 2019 Community

    call "C:\Program Files (x86)\Microsoft Visual Studio\2019\Community\VC\Auxiliary\Build\vcvars64.bat"
    %SIREUM_HOME%\bin\build.cmd native

  • Visual Studio 2017 Community

    call "C:\Program Files (x86)\Microsoft Visual Studio\2017\Community\VC\Auxiliary\Build\vcvars64.bat"
    %SIREUM_HOME%\bin\build.cmd native

To run:

• macOS:

  ${SIREUM_HOME}/bin/mac/sireum

• Linux:

  ${SIREUM_HOME}/bin/linux/sireum

• Windows:

  %SIREUM_HOME%\bin\win\sireum.exe

Note that once the native version is available (and has a newer timestamp), sireum and sireum.bat in bin call the native version. This is also similar for build.cmd in bin.

Dependencies

Sireum depends on open source software libraries and applications (the specific versions are listed in versions.properties).

Library Dependencies

Library	Maven	License
ANTLR3 Runtime	(link)	BSD3
ASM	(link)	BSD3
Automaton	(link)	BSD3
Coursier	(link)	Apache 2.0
GitHub API	(link)	MIT
NuProcess	(link)	Apache 2.0
OS-Lib	(link)	MIT
Scala	(link)	Apache 2.0
Scalameta	(link)	BSD3
ScalaTest	(link)	Apache 2.0
Scala Java 8 Compatibility Kit	(link)	Apache 2.0
Scala Parallel Collection	(link)	Apache 2.0
Scala.js	(link)	Apache 2.0
Scala.js: DOM	(link)	MIT
Scala.js: Scalatags	(link)	MIT

In addition, Sireum includes adaptation of the following artifact:

Source	Adaptation	License
ANTLRv3.g	SireumAntlr3.g	BSD3
diff_match_patch.java	DiffMatchPatch	Apache 2.0
Geny	Jen & MJen	MIT
SHA3IUF	SHA3	MIT
UnsafeUtils	UnsafeUtils	MIT

Application Dependencies

Application	License
Azul Zulu JDK FX	GPL v2 with "Classpath" exception
CVC4/5	BSD3
Z3	MIT

Sireum stores small, pre-built binary executables in its submodule repositories for macOS, Linux, and Windows (please see the respective repository for virus analysis results).

Pre-built Executable	License
7-zip	LGPL v2
fsnotifier	Apache 2.0
pts-tiny-7z-sfx	GPL v2
upx	GPL v2

Optional Application Dependencies

Application	License
checkstack.pl	GPL v2
GraalVM	GPL v2 with "Classpath" exception
IntelliJ	Apache 2.0
JetBrains Runtime	GPL v2 with "Classpath" exception
Mill	MIT
OSATE2	EPL 2.0

IntelliJ Plugin	License
ANTLR4	BSD3
ASM	Apache 2.0
JDT AstView	BSD2
Projector	GPL v2 with "Classpath" exception
ReStructuredText	Apache 2.0
Scala	Apache 2.0
Sireum	BSD2
Slang Injector	BSD2