Welcome > Logics > Fm in Arch > Spec Sail

Spec Sail

References:

RISCV Sail on Github
Using Sail Specifications in Isabelle/HOL, August 29, 2018. pdf

Sail Goals: engineer-friendly, vendor-pseudocode-like language for describing instruction semantics.

Sail: a first-order imperative language, but with lightweight dependent typing for numeric types and bitvector lengths.

Side-effects: Sail use its effect system to determine whether a function has side-effects and needs to be monadic.

Monadic function:

All about monads:
- Monads is a way to structure computations in terms of values and sequences of computations using typed values.
- Monads are strategies for solving coding problems that recur often, regardless of what you are writing.
- More than this, monads help make strategies composable: Combining computations into more complex computations.
- Examples: Maybe type, the List, and I/O are monads (in Haskell).
  - List solves a common problem: you need a very basic collection of items of the same type, with some easy-to-understand behavior and performance characteristics.
  - Maybe type: rescues you from having to write lots of null pointer checks – or else debug code that does not have enough of them.
  - I/O makes it possible to interact with a program at all.
a monadic function is a function with a single argument, written to its right. cite
A short and simple answer: a monadic function is one whose return data signature/type is the same as its input data signature/type. cite
Monad – Computation Builder: monad is a pattern for chaining operations. It looks a bit like method chaining in object-oriented languages, but the mechanism is slightly different. The pattern can be used in any language which support higher-order functions (that is, functions which can take other functions as arguments). cite

Sail with Isabelle

Sail Spec:

a decode function: map from raw instruction opcodes to a more abstract representation,
an execute function specifying the behaviour of instructions,
further auxiliary functions, and

Sail --> Lem --> Isabelle/HOL
         |--> HOL4

Translate to lem from Sail using -lem option:

sail -lem -o riscv_duopod -lem_mwords -lem_lib Riscv_extras preclude.sail riscv_duopod.sail

-lem activates the generation of Lem def.

-o riscv_duopod specifies the prefix of output, it will generate files:

- `riscv_duopod_types.lem`, types used in the defs;
- `riscv_duopod.lem`, main definitions, e.g., of the instructions;
- `Riscv_duopod_lemmas.thy`, generated helper lemmas;

-lem_mwords: use the machine word representation of bitvectors.

-lem_lib Riscv_extras: Lem lib to be imported.

Translate from Lem to Isabelle, using -isa option:

lem -isa -outdir . -lib Sail=../src/lem_interp -lib Sail=../src/gen_lib riscv_extras.lem riscv_duopod_types.lem riscv_duopod.lem

Isabelle Examples:

Abstract syntax

Abstract syntax:

datatype ast = ITYPE (12 word * 5 word * 5 word * iop)
    | LOAD (12 word * 5 word * 5 word)

Decode function

Decode function: decode :: 32 word ==> ast option.

decode function is pure. (Sail use its effect system to determine whether a function has side-effects and needs to be monadic.)
```
decode opcode = (if-then-else-cascade)
```

Execute function

Execute function: is monadic.

execute-LOAD imm rs rd = 
 rX (regbits-to-regno rs) >>=
 ($\lambda$w--0. 
    let addr = add-vec w--0 (EXTS 64 imm)
    in MEMr0 addr 8 >>= wX (regbits-to-regno rd)
 )

==> reads the base addr from the source register rs, then adds the offset in the immediate argument imm, calls the MEMr auxiliary function to read 8 bytes starting at the calculated address, and writes the result into the destination register d.

Auxiliary functions

Auxiliary functions: dispatch inputs to auxiliary functions.

execute (ITYPE (imm1, rs1, rd1, arg3.0)) = execute-ITYPE imm1 rs1 rd1 arg3.0
execute (LOAD (imm, rs, rd)) = execute-LOAD imm rs rd

Register declarations

regstate record gets generated from register declarations in Sail source code:

record regstate = 
  Xs :: (64 Word.word) list
  nextPC :: 64 Word.word
  PC :: 64 Word.word

==> In RISC-V spec, the general-purpose register file is declared as one register Xs containing the 32 registers and 64 bits each. It gets mapped to a list of 64-bit words.

Monads for concurrent reasoning

Concurrent: free monad of an effect datatype that provides fine-grained information about the register and memory effects of monadic expressions, suitable for integration with relatex memory models.

Monads for sequential reasoning

Sequential case: we use a state monad (with exceptions and nondeterminism)

Example in Isabelle – ADDI

Goal: prove that the add instruction in RISC-V duopod actually performs an addition.

The ADDI def in isabelle:

addi def

Sequential case, use state monad.

Sail.Hoare:

{|precondition P|} monadic expression f {| postcondition Q |}

hoare logic1

{|precondition P|} monadic expression f {| postcondition Q | exceptions E |}

hoare logic2 with exception

Proof:

lemmas-1 lemmas-2

Step1: Simplication: unfolds the definitions of the auxiliary functions rX and wX, performs the lifting from the free monad to the state monad;

Step2: Apply the rule PrePostE-strengthen-pre (in backward manner) to allow a weaker precondition;

Step3: Use the rules in PrePostE-compositeI and PrePostE-atomI to derive a weakest precondition;

Step4: Use auto to show that it is implied by the given precondition.

For more serious proofs, one will want to set up specialized proof tactics. This example uses only basic proof methods, to make the reasoning steps more explicit.

Sail with Coq

A direct Sail-to-Coq backend.

Islaris: Verification of Machine Code Against Authoritative ISA Semantics

References: Islaris: verification of machine code against authoritative ISA semantics Problem Machine code verification: some critical code manipulates arch features that are not exposed in higher-level languages, e.g., to access system registers to install exception vector tables, or to configure address translation; this is necessarily written in assembly. verification without needing trust or verification of any compilation or assembly steps. verify the machine code after any modifications introduced by linking or initialisation (perhaps parametrically w.

RISCV in Sail

References: Sail RISCV Reading Guide Extending the model RISCV Sail Definitions in directory model/ ./model/ (files in dependency order) … riscv_xlen32.sail: define xlen for RV32 riscv_xlen64.sail: define xlen for RV64 … prelude.sail : constains Sail library functions prelude_mapping.sail : prelude_mem.sail : defines lowest level memory access primitives. These primitives will be implemented by the various Sail backends. This depends on the value of xlen prelude_mem_metadata.sail : … riscv_types.

If you could revise
the fundmental principles of
computer system design
to improve security...

... what would you change?