Spike Tag - RISC-V ISA Simulator with Information Flow Tracking

About

Spike Tag is a RISC-V ISA Simulator that supports information flow tracking by tagging program data. It is an extension of the Spike simulator.

Spike tag supports the following RISC-V ISA extensions:

• RV32I and RV64I base ISAs
• RV32E and RV64I base ISAs
• A extension
• C extension
• M extension
• F extension
• D extension
• Zfh extension
• Q extension
• Supervisor and User modes

The program uses input files that are generated by tag-parser, a program that takes the tag and policy files and generates apropriate files that the simulator uses.

Build Steps

We assume that the RISCV environment variable is set to the RISC-V tools install path.

$ apt-get install device-tree-compiler
$ mkdir build
$ cd build
$ ../configure --prefix=$RISCV
$ make
$ [sudo] make install

If your system uses the yum package manager, you can substitute yum install dtc for the first step.

Compiling and Running a Simple C Program

Install spike-tag (see Build Steps), riscv-gnu-toolchain, riscv-pk and tag-parser.

Write a short C program and name it hello.c. Then, compile it into a RISC-V ELF binary named hello:

$ riscv64-unknown-elf-gcc -o hello hello.c

Write the tag and policy files and run the tag parser:

$ tag-parser hello hello.tags hello.policy

Now you can simulate the program atop the proxy kernel:

$ spike-tag --tag-files=policy.mtag,tags.mtag pk hello

Interactive Debug Mode

To invoke interactive debug mode, launch spike with -d:

$ spike-tag --tag-files=policy.mtag,tags.mtag -d pk hello

To see the contents and the tag of an integer register (0 is for core 0):

: reg 0 a0

To see the contents of a floating point register:

: fregs 0 ft0

or:

: fregd 0 ft0

depending upon whether you wish to print the register as single- or double-precision.

To see the contents of a memory location (physical address in hex):

: mem 2020

To see the contents of memory with a virtual address (0 for core 0):

: mem 0 2020

You can advance by one instruction by pressing the enter key. You can also execute until a desired equality is reached:

: until pc 0 2020                   (stop when pc=2020)
: until reg 0 mie a                 (stop when register mie=0xa)
: until mem 2020 50a9907311096993   (stop when mem[2020]=50a9907311096993)

Alternatively, you can execute as long as an equality is true:

: while mem 2020 50a9907311096993

You can continue execution indefinitely by:

: r

At any point during execution (even without -d), you can enter the interactive debug mode with <control>-<c>.

To end the simulation from the debug prompt, press <control>-<c> or:

: q