Sireum aims to provide basic building blocks, frameworks, and tools to engineer high assurance systems by employing various formal method techniques for system validation and verification (V&V) at different stages of system development cycle such as architectural designs and system implementations.

Central to its approach is Slang – the Sireum programming language, a modern language designed first for formal safety and security analyses. Slang is (currently) realized as a subset of the Scala programming language with customized semantics designed to ease program reasoning. As a subset of Scala, Slang benefits from Scala’s rich and highly abstract language features, as well as extensive Scala and Java tooling, including IDEs and compiler toolchains for multiple platform targets such as JVM, Javascript, and native code. Moreover, Sireum provides a translation to C from a subset of Slang – Slang Embedded, which is specifically designed for embedded systems, without requiring garbage collection at runtime. The generated C code can be compiled using standard C compilers such as clang and gcc, as well as using the CompCert verified C compiler. In addition, a slight customization of the C translation can be used synthesize hardware by using existing high-level synthesis tools. Furthermore, Sireum provides a compositional, incremental, and parallel build tool – Proyek, and a customized IntelliJ version – Sireum IVE (Integrated Verification Environment), specifically set up for Slang and with other Sireum framework/tool integrations.

One example integration is for Logika – the Sireum verification framework. Logika provides highly automated Slang behavioral contract verification with interactive theorem proving support, focusing on its usability and scalability. On usability, Logika ensures continuity of user experience by keeping users focused at the Slang level such as for its quick verification feedback and theorem proving interactions in Sireum IVE. Logika’s scalability is achieved by its compositional reasoning approach (note that Logika can also verify programs inter-procedurally), incremental verification, and massive parallelization (and in the future, distributed computing). As a framework, Logika can be extended to integrate with other theorem provers or proof assistants to benefit from their strengths. In addition, Logika provides extension points to customize its verification engine. One such example is Logika’s customization to verify secure condition information flow in InfoFlow.

Another Sireum key component is HAMR, which provides static analysis, verification, code generation, and testing framework for AADL component-based system architectural models. HAMR defines a high assurance subset for AADL with formalized semantics to ease analyses and verification. HAMR leverages Slang for code generation and testing (via staged compilation), thus enabling it to generate high assurance AADL runtime services (middleware) for a system architecture to multiple target platforms, including for deployment using the seL4 verified micro-kernel. HAMR leverages Logika for verifying AADL interface contracts and translates AADL contracts to Slang contracts as it generates AADL runtime services, thus enabling verification of system component implementations. In addition to AADL, HAMR can also be retooled to support SysML V2 (see HAMR SysMLv2).