This directory holds the Latex source files for the specification of trusted LFI components: the verifier and the runtime. A PDF version of this specification can be found online.
This specification should be considered a draft. However, it is the most up-to-date documentation on the current LFI schemes for Arm64 and x86-64.
A specification for untrusted LFI components is also in-progress. That specification will describe the behavior of the LFI rewriter, which can be used by compiler developers to produce programs that pass the LFI verifier.
The Latex template used for this specification was adapted from the Hare language specification.