diff --git a/.gitignore b/.gitignore index 6b847442..637468b7 100644 --- a/.gitignore +++ b/.gitignore @@ -3,3 +3,4 @@ /requirements/export /target result +whitepaper/main.pdf diff --git a/flake.lock b/flake.lock index e9f48e5c..21b3ce75 100644 --- a/flake.lock +++ b/flake.lock @@ -76,6 +76,22 @@ "type": "github" } }, + "nixpkgs-unstable": { + "locked": { + "lastModified": 1731139594, + "narHash": "sha256-IigrKK3vYRpUu+HEjPL/phrfh7Ox881er1UEsZvw9Q4=", + "owner": "nixos", + "repo": "nixpkgs", + "rev": "76612b17c0ce71689921ca12d9ffdc9c23ce40b2", + "type": "github" + }, + "original": { + "owner": "nixos", + "ref": "nixos-unstable", + "repo": "nixpkgs", + "type": "github" + } + }, "nixpkgs_2": { "locked": { "lastModified": 1731239293, @@ -98,7 +114,10 @@ "fenix": "fenix", "naersk": "naersk", "nixpkgs": "nixpkgs_2", + "nixpkgs-unstable": "nixpkgs-unstable", "treefmt-nix": "treefmt-nix", + "typix": "typix", + "typst-packages": "typst-packages", "utils": "utils" } }, @@ -154,6 +173,42 @@ "type": "github" } }, + "typix": { + "inputs": { + "nixpkgs": [ + "nixpkgs-unstable" + ] + }, + "locked": { + "lastModified": 1731352170, + "narHash": "sha256-2JOC9lrFa0NfP9kfaT3dnm8WG5yAeDPONHJeMYl+O60=", + "owner": "loqusion", + "repo": "typix", + "rev": "7365cb7e6665350cb7b013abba1cbb70fcf07c53", + "type": "github" + }, + "original": { + "owner": "loqusion", + "repo": "typix", + "type": "github" + } + }, + "typst-packages": { + "flake": false, + "locked": { + "lastModified": 1731485222, + "narHash": "sha256-uhXDznbGLS4s6d2S8OHUCzpgmJQ1H2HCJug7kRIY0Jw=", + "owner": "typst", + "repo": "packages", + "rev": "4979ee3923fb0143e5d076854cb0d94bbf367a2c", + "type": "github" + }, + "original": { + "owner": "typst", + "repo": "packages", + "type": "github" + } + }, "utils": { "inputs": { "systems": "systems" diff --git a/flake.nix b/flake.nix index ea75a4cd..d95c7100 100644 --- a/flake.nix +++ b/flake.nix @@ -3,6 +3,15 @@ inputs = { nixpkgs.url = "github:nixos/nixpkgs/nixos-24.05"; + nixpkgs-unstable.url = "github:nixos/nixpkgs/nixos-unstable"; + typst-packages = { + url = "github:typst/packages"; + flake = false; + }; + typix = { + url = "github:loqusion/typix"; + inputs.nixpkgs.follows = "nixpkgs-unstable"; + }; utils.url = "git+https://github.com/numtide/flake-utils.git"; devshell.url = "github:numtide/devshell"; fenix = { @@ -24,7 +33,14 @@ lib = nixpkgs.lib; pkgs = import nixpkgs { inherit system; - overlays = [ devshell.overlays.default ]; + overlays = [ + devshell.overlays.default + + # We unfortunately need the most up-to-date typst + (final: prev: { + typst = inputs.nixpkgs-unstable.legacyPackages.${pkgs.hostPlatform.system}.typst; + }) + ]; }; # universal formatter @@ -36,16 +52,15 @@ # Rust distribution for our hostSystem fenix = inputs.fenix.packages.${system}; - rust-toolchain = with fenix; - combine [ - latest.rustc - latest.cargo - latest.clippy - latest.rustfmt - targets.${rust-target}.latest.rust-std - targets.thumbv6m-none-eabi.latest.rust-std # for no_std test - targets.wasm32-unknown-unknown.latest.rust-std - ]; + rust-toolchain = with fenix; combine [ + latest.rustc + latest.cargo + latest.clippy + latest.rustfmt + targets.${rust-target}.latest.rust-std + targets.thumbv6m-none-eabi.latest.rust-std # for no_std test + targets.wasm32-unknown-unknown.latest.rust-std + ]; # overrides a naersk-lib which uses the stable toolchain expressed above naersk-lib = (naersk.lib.${system}.override { @@ -53,14 +68,31 @@ rustc = rust-toolchain; }); + typstPackagesCache = pkgs.stdenv.mkDerivation { + name = "typst-packages-cache"; + src = inputs.typst-packages; + dontBuild = true; + installPhase = '' + mkdir -p "$out/typst/packages" + cp --dereference --no-preserve=mode --recursive --reflink=auto \ + --target-directory="$out/typst/packages" -- "$src"/packages/* + ''; + }; in { # packages packages.wasm-interpreter = pkgs.callPackage pkgs/wasm-interpreter.nix { }; + packages.whitepaper = inputs.typix.lib.${system}.buildTypstProject { + name = "whitepaper.pdf"; + src = ./whitepaper; + XDG_CACHE_HOME = typstPackagesCache; + }; + packages.report = pkgs.callPackage pkgs/report.nix { - inherit (self.packages.${system}) wasm-interpreter; + inherit (self.packages.${system}) wasm-interpreter whitepaper; }; + # a devshell with all the necessary bells and whistles devShells.default = (pkgs.devshell.mkShell { imports = [ "${devshell}/extra/git/hooks.nix" ]; @@ -84,6 +116,7 @@ nixpkgs-fmt nodePackages.prettier treefmtEval.config.build.wrapper + typst # for the whitepaper ]; env = [ { @@ -132,6 +165,13 @@ ''; help = "start cargo watch loop for documentation"; } + { + name = "whitepaper-watch"; + command = '' + typst watch --root "$PRJ_ROOT/whitepaper" "$PRJ_ROOT/whitepaper/main.typ" + ''; + help = "start typst watch loop for the whitepaper"; + } ]; }); diff --git a/pkgs/report.nix b/pkgs/report.nix index 0bf701bf..3efff931 100644 --- a/pkgs/report.nix +++ b/pkgs/report.nix @@ -1,4 +1,4 @@ -{ lib, stdenvNoCC, python3Packages, strictdoc, wasm-interpreter }: +{ lib, stdenvNoCC, python3Packages, strictdoc, wasm-interpreter, whitepaper }: let evidenceRoot = lib.strings.escapeShellArg wasm-interpreter; @@ -22,6 +22,7 @@ stdenvNoCC.mkDerivation { cp --recursive -- ${evidenceRoot}/bench-html bench cp --recursive -- ${evidenceRoot}/lcov-html coverage cp --recursive -- ${evidenceRoot}/share/doc/ rustdoc + cp --dereference -- ${whitepaper} whitepaper.pdf mkdir test junit2html ${evidenceRoot}/junit.xml test/index.html diff --git a/pkgs/report_index.html b/pkgs/report_index.html index 5dd9d289..d8be26f0 100644 --- a/pkgs/report_index.html +++ b/pkgs/report_index.html @@ -47,5 +47,6 @@ Tests Coverage Benchmark + Whitepaper diff --git a/treefmt.nix b/treefmt.nix index 6de2f3e8..6754f37a 100644 --- a/treefmt.nix +++ b/treefmt.nix @@ -24,4 +24,5 @@ }; }; programs.rustfmt.enable = true; + programs.typstfmt.enable = true; } diff --git a/whitepaper/main.typ b/whitepaper/main.typ new file mode 100644 index 00000000..c5efa4e7 --- /dev/null +++ b/whitepaper/main.typ @@ -0,0 +1,150 @@ +/* imports */ +#import "@preview/acrostiche:0.4.0": * +#import "@preview/ccicons:1.0.0": * + +/* variables and setup */ +#let title = [WASM Interpreter for Safety -- White Paper] + +/* TODO make this multi-author capable */ +#let author = "Wanja Zaeske" +#let affiliation = [ + Department Safety Critical Systems & Systems Engineering \ + German Aerospace Center (DLR) \ + #link("mailto:wanja.zaeske@dlr.de") +] + +#set document( + title: title, author: author, keywords: ("WebAssembly", "Safety-Critical"), +) + +#init-acronyms( + ( + "AOT": ("Ahead-of-time"), "DAL": ("Design Assurance Level"), "DARPA": ("Defense Advanced Research Projects Agency"), "IR": ("Intermediate Representation"), "JIT": ("Just-in-time"), "SBOM": ("Software Bill of Materials"), "TQL": ("Tool Qualification Level"), "TRACTOR": ("Translating All C to Rust"), "WASM": ("WebAssembly"), + ), +) + +/* style */ +#set page( + paper: "a4", header: context{ + if counter(page).get().first() > 1 [ + #align(right, title), + ] + }, footer: context[ + #set text(8pt) + License: #link("https://creativecommons.org/licenses/by-sa/4.0/")[CC-BY-SA #cc-by-sa] + #h(1fr) #counter(page).display("1 of 1", both: true) \ + + Copyright © 2024-#datetime.today().year() German Aerospace Center (DLR). All + rights reserved. + ], columns: 1, +) + +#set heading(numbering: "1.") + +#align(center, text(17pt)[*#title*]) + +#grid(columns: (1fr), align(center)[ + #author \ + #affiliation +]) + += Introduction +This white paper provides an overview over our WebAssembly interpreter +@our-repo. It Primarily serves to highlight and explain design decisions and the +goals we aim to achieve. + +The development of this project currently takes place as a joint effort between +DLR-ft @dlr-ft-website and OxidOS @oxidos-website. Being truly Open Source, the +project already is willing to accept external contributions. As the project +matures, it might be worth considering moving the project to a vendor-agnostic +foundation, to assure for a fair process allowing contributions from multiple +commercial entities. However, for the time being the project is not mature +enough to justify the overhead doing so, thus for the time being the project +remains under control of DLR & OxidOS. + +== Design Drivers +The implementation of our interpreter is driven by several design goals. After +all, there are dozens of WebAssembly interpreters around, why would one have to +implement yet another one? + +=== Pure Interpretation +In fact, the prior sentence is somewhat imprecise. Most WebAssembly interpreters +are actually compilers; they compile the WebAssembly down to a different format +that seems more suitable for execution. A prominent example would be WasmTime +@wasmtime-website, which compiles WebAssembly down to object code, so called #acr("AOT") compilation. +Browsers commonly mix in #acr("JIT") compilation as well, starting with a +quick-to-compile but not so fast-to-run #acr("AOT") baseline build, which then +on demand is partially swapped for optimized sections obtained by #acr("JIT") compiling +code sections in the hot path (example: @mozilla-baseline-compiler). + +But even if neither #acr("AOT") nor #acr("JIT") are at hand (no object code for +the physical processor is created), there still is a common pattern of rewriting +the #acr("WASM") bytecode into a custom #acr("IR") (example: +@wasmi-instruction-enum). There are multiple reasons for this, this allows for +gentle optimizations, simpler code, and foremost explicit jumps. In ordinary #acr("WASM") bytecode, +branches are indirect; e.g. a branch could be "jump out of the innermost three +scopes". In practical terms, a branch boils down to modifying the program +counter/instruction pointer, i.e. advance it 15 instructions forward. To avoid +costly linear search at runtime (for where the innermost three scopes end), many +interpreters rewrite the #acr("WASM") bytecode into their own #acr("IR"), +calculating the direct offsets on the instruction pointer for the branches once, +so that in their #acr("IR") branches are direct. + +This is a good decision for many use-cases, but tricky when safety-certification +comes into play. Now, the currency in safety certification is evidence, and for +the special case of avionics, a significant amount of evidence has to be +provided for the object code @webassembly-in-avionics-paper. Thus, generating +object code at run-time (for example when #acr("JIT") compiling) is prohibitive +-- it simply does not fit together with the assumptions baked into current +certification guidelines such as DO-178C @do178c. Finally, DO-332 contains +specific language that allows for the directly interpreted format executed by a +virtual machine/bytecode interpreter to be treated as object code. Hence, when +compiling #acr("WASM") bytecode into a custom #acr("IR"), one would have to +provide certification evidence on that #acr("IR"). + +Our design alleviates all this; by directly interpreting the #acr("WASM") bytecode, +certification evidence has to be produced for the #acr("WASM") directly, and +thus is not tied to implementation details (as in particular #acr("IR")) used by +our interpreter. A comprehensive discussion of this can be found in our +publication @webassembly-in-avionics-paper. + +To avoid the problem of indirect branching, we borrow ideas from Ben L. Titzer's +wizard @wizard-engine, a pre-computed side-table that for all branches stores +the direct offset on the instruction pointer. A detailed discussion of the +technique and further implementation details of wizard can be found in his paper +@fast-in-place-interpreter-for-webassembly. + +=== Certification Friendly Source Code +Our implementation is written in Rust, which on its own poses a challenge: As of +now, we are not aware of any high-assurance deployment of Rust in the aviation +sector. Similarly, there is only little information on Rust being deployed in +automotive (such as @volvo-rust-assembly-line). At the same time, there is a +keen interest to push Rust in safety critical domains, and companies like +ferrous systems @ferrous-systems-website with their ISO 26262 ASIL D certified +Rust compiler @ferrocene-website and AdaCore with the GNAT Pro for Rust +@adacore-rust-website pave the way for Rust. + +Now, there some techniques often found in Rust programs pose risk for a smooth +certification. One such thing would be macros. While we are not aware of a +precedence case, we assume that Rust's various flavors of macros might be +treated like tools, after all they are computer programs that generated code, +which in term is compiled in to the final application. As such, they might be +subject to tool qualification as per DO-330 @do330, and in since macros can +easily sneak in broken code, they are likely to be treated as criteria 1 tool +@do330. If these assumptions hold, macros would have to be tool qualified to the +matching #acr("TQL") of an application's #acr("DAL"). As testing macros is more +complicated than testing normal code, we restrict our usage of macros to the +bare minimum. + +Another risk to certification is third party code. Thus, to keep our code +closure (and subsequently the #acr("SBOM") compact), we refrain from using +dependencies which get compiled into the code#footnote[Currently, two carefully selected run-time dependencies are allowed, however, + there is a roadmap to phase them out, and each such exception is tracked in our + requirements]. + +/* +TODO talk about Nix +=== Infrastructure as Code wherever possible +*/ + +#bibliography("refs.yaml") diff --git a/whitepaper/refs.yaml b/whitepaper/refs.yaml new file mode 100644 index 00000000..01724152 --- /dev/null +++ b/whitepaper/refs.yaml @@ -0,0 +1,148 @@ +# Heper to convert from BibTeX: +# https://jonasloos.github.io/bibtex-to-hayagriva-webapp/ + +# papers + +webassembly-in-avionics-paper: + type: article + title: "WebAssembly in Avionics : Decoupling Software from Hardware" + author: + - Zaeske, Wanja + - Friedrich, Sven + - Schubert, Tim + - Durak, Umut + date: 2023 + page-range: 1–10 + serial-number: + doi: 10.1109/DASC58513.2023.10311207 + parent: + type: proceedings + title: 2023 IEEE/AIAA 42nd Digital Avionics Systems Conference (DASC) + issue: "" + volume: 0 + +fast-in-place-interpreter-for-webassembly: + type: article + title: A fast in-place interpreter for WebAssembly + author: Titzer, Ben L. + date: 2022-10 + url: https://doi.org/10.1145/3563311 + serial-number: + doi: 10.1145/3563311 + parent: + type: periodical + title: Proc. ACM Program. Lang. + publisher: Association for Computing Machinery + location: New York, NY, USA + issue: OOPSLA2 + volume: 6 + +# standards etc. + +do178c: + type: report + title: "{DO-178C} Software Considerations in Airborne Systems and Equipment Certification" + author: RTCA + date: 2011 + organization: RTCA +do330: + type: report + title: "{DO-330} Software Tool Qualification Considerations" + author: RTCA + date: 2011 + organization: RTCA + +do331: + type: report + title: "{DO-331} Model-Based Development and Verification Supplement to {DO-178C} and {DO-278A}" + author: RTCA + date: 2011 + organization: RTCA + +do332: + type: report + title: "{DO-332} Object-Oriented Technology and Related Techniques Supplement to {DO-178C} and {DO-278A}" + author: RTCA + date: 2011 + organization: RTCA + +do333: + type: report + title: "{DO-333} Formal Methods Supplement to {DO-178C} and {DO-278A}" + author: RTCA + date: 2011 + organization: RTCA + +# websites + +our-repo: + type: Web + title: wasm-interpreter + author: + - DLR e. V. + - OxidOS + url: https://github.com/DLR-FT/wasm-interpreter + +dlr-ft-website: + type: Web + title: DLR | Institute of Flight Systems + author: DLR e. V. + url: https://www.dlr.de/en/ft + +oxidos-website: + type: Web + title: Welcome to OxidOS Automotive + author: OxidOS + url: https://oxidos.io/ + +wasmtime-website: + type: Web + title: A fast and secuire runtime for Webassembly + author: Bytecode Alliance + url: https://wasmtime.dev/ + +mozilla-baseline-compiler: + type: Web + title: "Making WebAssembly even faster: Firefox’s new streaming and tiering compiler" + author: Lin Clark + url: https://hacks.mozilla.org/2018/01/making-webassembly-even-faster-firefoxs-new-streaming-and-tiering-compiler/ + +wasmi-instruction-enum: + type: Web + title: "Making WebAssembly even faster: Firefox’s new streaming and tiering compiler" + author: Robin Freyler et al. + url: https://docs.rs/wasmi_ir/latest/wasmi_ir/enum.Instruction.html + +wizard-engine: + type: Web + title: The Wizard Research Engine + author: Ben L. Titzer et al. + url: https://github.com/titzer/wizard-engine + +volvo-rust-assembly-line: + type: Web + title: Rust is rolling off the Volvo assembly line + author: + - Dion Dokte + - Julius Gustavsson + url: https://tweedegolf.nl/en/blog/137/rust-is-rolling-off-the-volvo-assembly-line + +ferrous-systems-website: + type: Web + title: Ferrous Systems + url: https://ferrous-systems.com/ + +ferrocene-website: + type: Web + title: This is Rust for critical systems. + url: https://ferrocene.dev/ + +adacore-website: + type: Web + title: AdaCore + url: https://www.adacore.com/ + +adacore-rust-website: + type: Web + title: GNAT Pro for Rust + url: https://www.adacore.com/gnatpro-rust