11 implement component mission protection system

.gitmodules

@@ -1,6 +1,3 @@
-[submodule "components/mission_protection_system/HARDENS"]
-	path = components/mission_protection_system/HARDENS
-	url = [email protected]:GaloisInc/HARDENS.git
 [submodule "src/pkvm_setup/linux-pkvm"]
 	path = src/pkvm_setup/linux-pkvm
 	url = https://github.com/rems-project/linux

components/mission_protection_system/HARDENS/.gitignore

@@ -0,0 +1,21 @@
+*/#*#
+*/.*
+*.o
+*.a
+*.bc
+*.ll
+*.elf
+*.asm
+.vscode
+src/wp-session/
+src/generated/SystemVerilog/verilator/
+src/handwritten/SystemVerilog/verilator/
+src/self_test_data/
+src/rts*
+saw/*.v
+Assurance.pdf
+README.pdf
+Toolchain.pdf
+Specifications.pdf
+hardware/SoC/design.*
+tests/__pycache__/

components/mission_protection_system/HARDENS/hardware/SoC/firmware/Makefile

@@ -0,0 +1,112 @@
+TARGET=riscv64-unknown-elf
+ARCH 		= -march=rv32i
+ABI 		= -mabi=ilp32
+CC =clang --target=riscv32
+OBJDUMP	= $(TARGET)-objdump
+OBJCOPY	= $(TARGET)-objcopy
+LD 		= $(TARGET)-gcc
+LDLIBS	 =  -lc -lgcc
+
+COMPILER_FLAGS = -mcmodel=medany
+
+# Use main_blinky as demo source and target file name if not specified
+PROG 	?= main
+CRT0	= boot.S
+# Optimize for size
+OPT = -Os
+
+# NOTE: why do we have different warnings setup?
+WARNINGS = -Wno-shift-op-parentheses -Wno-shift-count-overflow -Wpointer-arith -Wcast-align -Werror
+
+INCLUDES = -I. -I/opt/riscv/riscv64-unknown-elf/include
+
+APP_SRC = syscalls.c \
+	bsp.c printf.c
+
+ifeq ($(PROG),main)
+PROG_SRC = ../../../src/rv32_main.c
+INCLUDES += -I../../../src/include
+APP_SRC += \
+	../../../src/core.c \
+	../../../src/common.c \
+	../../../src/sense_actuate.c \
+	../../../src/components/instrumentation_common.c \
+	../../../src/variants/actuation_unit_generated_C.c \
+	../../../src/variants/actuator_generated_C.c \
+	../../../src/variants/instrumentation_handwritten_C.c \
+	../../../src/variants/saturation_generated_C.c \
+	../../../src/variants/actuation_unit_generated_SystemVerilog.c \
+	../../../src/variants/instrumentation_handwritten_SystemVerilog.c \
+	../../../src/variants/instrumentation_generated_SystemVerilog.c \
+	../../../src/variants/instrumentation_generated_C.c
+else
+PROG_SRC = firmware.c
+endif
+
+ASFLAGS  += -g $(ARCH) $(ABI) -Wa,-Ilegacy
+CFLAGS += $(OPT) -g3 $(ARCH) $(ABI) $(COMPILER_FLAGS) $(WARNINGS) $(INCLUDES) -DPRINTF_INCLUDE_CONFIG_H
+LDFLAGS	 += -Wl,-Bstatic,-T,sections.ld,--strip-debug -nostartfiles -nostdlib $(ARCH) $(ABI)
+
+
+ifneq ($(SELF_TEST_PERIOD_SEC),)
+CFLAGS += -DSELF_TEST_PERIOD_SEC=$(SELF_TEST_PERIOD_SEC)
+endif
+
+SELF_TEST ?= Enabled
+
+ifeq ($(SELF_TEST),Enabled)
+CFLAGS += -DENABLE_SELF_TEST
+endif
+
+DEBUG_PRINT ?= Disabled
+
+ifeq ($(DEBUG_PRINT),Enabled)
+CFLAGS += -DDEBUG
+endif
+
+CLEAR_SCREEN ?= Enabled
+ifeq ($(CLEAR_SCREEN),Enabled)
+CFLAGS += -DCLEAR_SCREEN=1
+else
+CFLAGS += -DCLEAR_SCREEN=0
+endif
+
+CORE_FREQ ?= 100000
+CFLAGS += -DCORE_FREQ=$(CORE_FREQ)
+$(info CORE_FREQ=$(CORE_FREQ))
+
+#
+# Define all object files.
+#
+APP_OBJ  = $(APP_SRC:.c=.o)
+PROG_OBJ = $(PROG_SRC:.c=.o)
+CRT0_OBJ = $(CRT0:.S=.o)
+OBJS = $(CRT0_OBJ) $(PROG_OBJ) $(APP_OBJ)
+
+$(info ASFLAGS=$(ASFLAGS))
+$(info LDLIBS=$(LDLIBS))
+$(info CFLAGS=$(CFLAGS))
+$(info LDFLAGS=$(LDFLAGS))
+
+%.o: %.c
+	@echo "    CC $<"
+	@$(CC) -c $(CFLAGS) -o $@ $<
+
+%.o: %.S
+	@echo "    CC $<"
+	@$(CC) $(ASFLAGS) -c $(CFLAGS) -o $@ $<
+
+all: firmware.elf
+
+firmware.elf  : $(OBJS) Makefile
+	@echo Linking....
+	@$(LD) -o $@ $(LDFLAGS) $(OBJS) $(LDLIBS)
+	@$(OBJDUMP) -S -D firmware.elf > firmware.asm
+	@echo Completed $@
+
+clean :
+	@rm -f $(OBJS)
+	@rm -f *.elf
+	@rm -f *.asm
+	@find ../../../ -iname '*.o' -exec rm -rf {} \;
+

components/mission_protection_system/HARDENS/hardware/SoC/firmware/boot.S

@@ -0,0 +1,99 @@
+/*
+ *  NERV -- Naive Educational RISC-V Processor
+ *
+ *  Copyright (C) 2020  Claire Xenia Wolf <[email protected]>
+ *
+ *  Permission to use, copy, modify, and/or distribute this software for any
+ *  purpose with or without fee is hereby granted, provided that the above
+ *  copyright notice and this permission notice appear in all copies.
+ *
+ *  THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
+ *  WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
+ *  MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
+ *  ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
+ *  WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
+ *  ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
+ *  OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
+ *
+ */
+
+.section .text
+.global main
+.global _start
+_start:
+addi x1, zero, 0
+addi x2, zero, 0
+addi x3, zero, 0
+addi x4, zero, 0
+addi x5, zero, 0
+addi x6, zero, 0
+addi x7, zero, 0
+addi x8, zero, 0
+addi x9, zero, 0
+addi x10, zero, 0
+addi x11, zero, 0
+addi x12, zero, 0
+addi x13, zero, 0
+addi x14, zero, 0
+addi x15, zero, 0
+addi x16, zero, 0
+addi x17, zero, 0
+addi x18, zero, 0
+addi x19, zero, 0
+addi x20, zero, 0
+addi x21, zero, 0
+addi x22, zero, 0
+addi x23, zero, 0
+addi x24, zero, 0
+addi x25, zero, 0
+addi x26, zero, 0
+addi x27, zero, 0
+addi x28, zero, 0
+addi x29, zero, 0
+addi x30, zero, 0
+addi x31, zero, 0
+
+# copy data section
+la a0, _sidata
+la a1, _sdata
+la a2, _edata
+bge a1, a2, end_init_data
+loop_init_data:
+    lw a3, 0(a0)
+    sw a3, 0(a1)
+    addi a0, a0, 4
+    addi a1, a1, 4
+    blt a1, a2, loop_init_data
+end_init_data:
+
+init_bss:
+    /* init bss section */
+    la	a0, _sbss
+    la	a1, (_ebss-4) /* section end is actually the start of the next section */
+    li	a2, 0x0
+    jal	fill_block
+
+# write_stack_pattern:
+write_stack_pattern:
+    la	a0, _stack_end  /* note the stack grows from top to bottom */
+    la	a1, (__stack-4)   /* section end is actually the start of the next section */
+    li	a2, 0xABABABAB
+    jal	fill_block
+
+# initialize SP
+la	sp, _stack
+
+# call main
+call main
+
+# halt
+ebreak
+
+/* Fills memory blocks */
+fill_block:
+    sw		a2, 0(a0)
+    bgeu	a0, a1, fb_end
+    addi	a0, a0, 4
+    j		fill_block
+fb_end:
+    ret

components/mission_protection_system/HARDENS/hardware/SoC/firmware/bsp.c

@@ -0,0 +1,82 @@
+#include "bsp.h"
+#include "printf.h"
+
+uint32_t i2c_read(uint8_t addr, uint32_t data_tx)
+{
+  volatile uint32_t *i2c_addr = (void*) I2C_REG_ADDR;
+  volatile uint32_t *i2c_data = (void*) I2C_REG_DATA;
+  volatile uint32_t *i2c_status = (void*) I2C_REG_STATUS;
+
+  // First set data
+  *i2c_data = data_tx;
+  // Second set address
+  *i2c_addr = addr;
+  // Now the transaction is initialized, so wait for completion
+  delay(100);
+  while (1) {
+    uint32_t status = *i2c_status;
+    if (status) {
+      // Return the acquired data
+      uint32_t data = *i2c_data;
+      return data;
+    }
+    delay(1000);
+  }
+}
+
+uint32_t time_in_s(void)
+{
+  uint32_t t_s = time_in_ms()/1000;
+  return t_s;
+}
+
+uint32_t time_in_ms(void)
+{
+  volatile uint32_t *tick_reg_low = (void*) TICK_REG_LOW;
+  volatile uint32_t *tick_reg_high = (void*) TICK_REG_HIGH;
+  uint64_t ticks = (uint64_t) (*tick_reg_high << 31 | *tick_reg_low);
+  return (uint32_t)((ticks*1000)/(CORE_FREQ*TICKS_TO_MS_MULTIPLIER));
+}
+
+void delay_ms(uint32_t ms)
+{
+    uint32_t ticks = ms*CORE_FREQ/1000;
+    delay(ticks);
+}
+
+void delay(uint32_t count)
+{
+	while(count-->0) {
+		__asm__ volatile ("nop");
+	}
+}
+
+uint8_t soc_getchar(void)
+{
+  volatile uint32_t *data_rdy = (void*) UART_REG_DATA_READY;
+  volatile uint32_t *rx_data = (void*) UART_REG_RX;
+  int startime = time_in_ms();
+  int delay_ms = 0;
+  // Wait 1s for each character
+  while ((delay_ms < 2000)) {
+    if (*data_rdy){
+        return (uint8_t)(*rx_data);
+    }
+    delay_ms = time_in_ms() - startime;
+  }
+  return 0;
+}
+
+// Read from a register
+uint32_t read_reg(uint32_t reg)
+{
+  uint32_t *p = (void*)reg;
+  return *p;
+}
+
+// Write `val` to `reg`
+void write_reg(uint32_t reg, uint32_t val)
+{
+  uint32_t *p = (void*)reg;
+  *p = val;
+}