Ironclad: Unix-like operating system kernel written in SPARK and Ada

Ironclad is a partially formally verified real-time kernel, with a small footprint, for general-purpose and embedded OSes, written in SPARK and Ada.

Some of the supported features are:

• A familiar POSIX-compatible interface.
• True simultaneous multitasking.
• Resiliency and small footprint.
• Partial gold-level formal verification.
• Advanced cryptography and a security-centered architecture, including MAC.
• Hard real-time scheduling and real-time oriented features.
• Support for severals architectures and boards.

For more information about the project, some autogenerated documentation, bug reporting, and development guides, check https://ironclad-os.org

Building and testing

The tools needed are:

• standard *nix tools including find and GNU make.
• autoconf and automake when not using a tarball (for ./bootstrap).
• gprbuild for compilation, along with a compatible Ada compiler and assembler.
• GNU Info for building the documentation.
• highlight for syntax highlighting when building the HTML documentation.
• gnatprove for formal verification, if desired.
• typos for spell-checking, if desired.

If checking out Git sources instead of building from a tarball, run ./bootstrap first.

For building the project's binaries, a standard configure-make-make install is enough, like the following:

(Replace make with gmake or similar if necessary, on systems where GNU make is not the default make).

Several flags are provided in configure for customizing kernel settings, one can check them with ./configure --help.

The above would build Ironclad for the architecture of the host system; so for example it would be built for x86_64 on an x86_64 host. In order to cross compile Ironclad for a different architecture, one can use the standard autoconf option --host= for ./configure. For example: ./configure --host=riscv64-linux-gnu would build Ironclad for RISC-V 64-bit, using the riscv64-linux-gnu toolchain.

Additionally, the optional PLATFORM=... variable can be passed to ./configure to tell the build system which platform/board to build Ironclad for. So far, the only supported value for PLATFORM is limine, which is the default.

Contributing and bug reporting

Thanks for considering contributing to Ironclad, it means a lot.

Please check our contributing document for information on how to get started, how to submit patches to the project, and how to submit bugs.

For security vulnerabilities, or other security critical bugs, please follow the guidelines of our security policy.

You can visit our list of community channels on Ironclad's [community tab] (https://ironclad-os.org/community.html).

Thanks to

This project is funded through NGI Zero Core, a fund established by NLnet with financial support from the European Commission's Next Generation Internet program. Learn more at the NLnet project page.