Dependable Bits | High Assurance Systems
This document gives an overview of the core software infrastructure that kwatafana.org depends on.
This is a living document that changes with the times because software is like that ðĪŠ
You can find allot of brilliant code on the internet, skillful programmers pushing computers to the limits. Some code is written as a form of self expression â art or simply to make a statement in the fabric of consciousness.
The point is not all code is meant to be dependent on especially for safety critical applications. Dependencies should be picked with great care. This is an important principle for cyber-security. A rigorous analysis of your dependencies can be the best protection against supply-chain attacks. This also means that dependencies should be simple and minimal with a relatively small code surface to make it possible to analyze/audit. Sometimes this means that you would have to rewrite some components instead of depending on software that does not fit our methodology.
The general methodology we use to decide to depend on a piece of software:
License: We depend on Public domain, Open Source and Free Software
Age: The software should not be too old, because it might not be supported by modern platforms or have received security updates. The software should also not be too new and without enough running in the wild.
Code quality & Auditing: We prefer to use audited code, the auditor should preferably be a 3rd party and not related to the original author. This is particularly important for cryptography software. The code should be of high quality and integrity.
Test Suite: The software should be well tested with unit tests, end-to-end tests and extensive fuzzing. It also helps if there is benchmarks comparing it to alternatives.
Documentation: Well documented software is preferred, software with clear APIs and interfaces, it is also plus if the code itself is well commented.
Developer: Is the project sustainable, are there maintainers and are they well funded or even motivated to keep the software up to date and stable.
Ecosystem: Software should have a vibrant community and enough resources (docs, blog, vids, example code). It also helps if the software can be easily integrated with other software especially with our other dependencies.
Minimalism: Software should be simple, clear, frugal, modular and correct. see unix philosophy and suckless.
Rust is a modern programming language with built in features for safe systems programming. Rust is designed to eliminate classes of software bugs/vulnerabilities that have been historically difficult to prevent.
Rust is also fast and low-level like C/C++ but drastically safer and more ergonomic to write, making it an ideal candidate for high performance and secure systems software.
//TODO:
Rust reached v1.0 in 2015, so it is a relatively young language so at the time of this writing Rust is not yet formally verified, no specification exists and the Rust reference is incomplete. None the less, Rust is used being used by allot of professional companies from Google, Microsoft, Facebook and lots of crypto-currencies all of them use Rust for what is promises to bring to the table: safe, fast systems programming.
Rust is well tested at this point just not formally verified and specified making it unable to be used for safety-critical environments that need a language to be formally specified.
More info about ongoing Rust R&D in formal verification tooling:
Also checkout this wonderful book High Assurance Rust, which is a great inspiration for this document and some of the methodologies used at https://kwatafana.org/
https://gitlab.com/kwatafana/spinneret ___
https://lamport.azurewebsites.net/tla/tla.html
updated: 2024-11-07