Initial commit

.gitignore

@@ -0,0 +1,54 @@
+# ---> C
+# Prerequisites
+*.d
+
+# Object files
+*.o
+*.ko
+*.obj
+*.elf
+
+# Linker output
+*.ilk
+*.map
+*.exp
+
+# Precompiled Headers
+*.gch
+*.pch
+
+# Libraries
+*.lib
+*.a
+*.la
+*.lo
+
+# Shared objects (inc. Windows DLLs)
+*.dll
+*.so
+*.so.*
+*.dylib
+
+# Executables
+*.exe
+*.out
+*.app
+*.i*86
+*.x86_64
+*.hex
+
+# Debug files
+*.dSYM/
+*.su
+*.idb
+*.pdb
+
+# Kernel Module Compile Results
+*.mod*
+*.cmd
+.tmp_versions/
+modules.order
+Module.symvers
+Mkfile.old
+dkms.conf
+

LICENSE

@@ -0,0 +1,11 @@
+Copyright (c) 2022 flip. 
+
+Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:
+
+1. Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.
+
+2. Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution.
+
+3. Neither the name of the copyright holder nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

README.md

@@ -0,0 +1,20 @@
+# STORM: State Transition Online Runtime Monitor
+
+## Introduction
+
+This repository contains a proof-of-concept for monitoring
+correct execution order of an arbirary C program using a
+transition matrix.
+
+First, the program is abstracted as a state transition system.
+This transition system is then modeled as a state transition matrix.
+A state transition matrix determines the allowed state
+depending on the last state.
+States here are synonmous with program checkpoints.
+The advantage of modeling the expected program flow as a matrix
+is that branching behaviour can be described.
+
+Using this matrix, by storing the last state and given a
+current state, the runtime monitor can check if program execution
+is valid.
+

examples/bad_fsm/Makefile

@@ -0,0 +1,41 @@
+TARGET_EXEC ?= bad_fsm
+
+BUILD_DIR ?= ./build
+SRC_DIRS ?= src ../../src
+
+SRCS := $(shell find $(SRC_DIRS) -name *.cpp -or -name *.c -or -name *.s)
+OBJS := $(SRCS:%=$(BUILD_DIR)/%.o)
+DEPS := $(OBJS:.o=.d)
+
+INC_DIRS := $(shell find $(SRC_DIRS) -type d)
+INC_FLAGS := $(addprefix -I,$(INC_DIRS))
+
+CPPFLAGS ?= $(INC_FLAGS) -MMD -MP
+
+$(BUILD_DIR)/$(TARGET_EXEC): $(OBJS)
+	$(CC) $(OBJS) -o $@ $(LDFLAGS)
+
+# assembly
+$(BUILD_DIR)/%.s.o: %.s
+	$(MKDIR_P) $(dir $@)
+	$(AS) $(ASFLAGS) -c $< -o $@
+
+# c source
+$(BUILD_DIR)/%.c.o: %.c
+	$(MKDIR_P) $(dir $@)
+	$(CC) $(CPPFLAGS) $(CFLAGS) -c $< -o $@
+
+# c++ source
+$(BUILD_DIR)/%.cpp.o: %.cpp
+	$(MKDIR_P) $(dir $@)
+	$(CXX) $(CPPFLAGS) $(CXXFLAGS) -c $< -o $@
+
+
+.PHONY: clean
+
+clean:
+	$(RM) -r $(BUILD_DIR)
+
+-include $(DEPS)
+
+MKDIR_P ?= mkdir -p

examples/bad_fsm/src/main.c

@@ -0,0 +1,155 @@
+#include "storm.h"
+
+#include <stdlib.h>
+#include <stdio.h>
+#include <stdint.h>
+#include <stdbool.h>
+#include <string.h>
+
+typedef struct STORM_DECL(64) storm64_t;
+
+typedef enum
+{
+    STATE_I,
+    STATE_A,
+    STATE_B,
+    STATE_C,
+    STATE_D
+}
+testfsm_state_t;
+
+typedef struct
+{
+    testfsm_state_t m_state;
+    bool m_fi;
+} testfsm_t;
+
+storm64_t s_monitor;
+bool s_reset = false;
+char s_trace[255] = { '\0' };
+
+char * testfsm_state_to_str(const testfsm_state_t s)
+{
+    char *str = "unknown";
+    switch(s)
+    {
+        case STATE_I: str = "I"; break;
+        case STATE_A: str = "A"; break;
+        case STATE_B: str = "B"; break;
+        case STATE_C: str = "C"; break;
+        case STATE_D: str = "D"; break;
+    }
+
+    return str;
+}
+
+void process(testfsm_t *p_fsm, const bool input)
+{
+    testfsm_state_t nextState = p_fsm->m_state;
+    storm_event((storm_t*)&s_monitor, p_fsm->m_state);
+
+    switch(p_fsm->m_state)
+    {
+        case STATE_I:
+            if (!input)
+                nextState = STATE_A;
+            else
+                nextState = STATE_B;
+            if (p_fsm->m_fi)
+                nextState = STATE_D;
+            break;
+        case STATE_A:
+            if (!input)
+                nextState = STATE_D;
+            else
+                nextState = STATE_C;
+
+            if (p_fsm->m_fi)
+                nextState = STATE_A;
+            break;
+        case STATE_B:
+            nextState = STATE_C;
+            if (p_fsm->m_fi)
+                nextState = STATE_A;
+            break;
+        case STATE_C:
+            nextState = STATE_A;
+            if (p_fsm->m_fi)
+            {
+                if(input)
+                    nextState = STATE_D;
+                else
+                    nextState = STATE_B;
+            }
+            break;
+        case STATE_D:
+            nextState = STATE_B;
+            break;
+    }
+
+    p_fsm->m_state = nextState;
+}
+
+void on_violation(const testfsm_state_t now, const testfsm_state_t next)
+{
+    printf("ERROR: Illegal checkpoint transition (%s, %s)!\n",
+           testfsm_state_to_str(now),
+           testfsm_state_to_str(next));
+    s_reset = true;
+
+    // print trace
+    sprintf(s_trace, "%sX", s_trace);
+    printf("FSM trace: %s\n\n", s_trace);
+    memset(s_trace, '\0', sizeof(s_trace));
+}
+
+bool randbool(int throws)
+{
+    bool stillTrue = true;
+    for (int i = 0; i < throws; ++i)
+    {
+        stillTrue &= rand() & 1;
+    }
+    return stillTrue;
+}
+
+int main()
+{
+    testfsm_t fsm = { .m_state = STATE_I, .m_fi = false };
+    bool input = false;
+
+    srand(0);
+    printf("Testing\n");
+    storm_init((storm_t*)&s_monitor, STATE_I, 64,
+               (storm_violation_hook_t)on_violation);
+    
+    // init allowed transitions
+    storm_allow((storm_t*)&s_monitor, STATE_I, STATE_I);
+    storm_allow((storm_t*)&s_monitor, STATE_I, STATE_A);
+    storm_allow((storm_t*)&s_monitor, STATE_I, STATE_B);
+    storm_allow((storm_t*)&s_monitor, STATE_A, STATE_C);
+    storm_allow((storm_t*)&s_monitor, STATE_A, STATE_D);
+    storm_allow((storm_t*)&s_monitor, STATE_B, STATE_C);
+    storm_allow((storm_t*)&s_monitor, STATE_C, STATE_A);
+    storm_allow((storm_t*)&s_monitor, STATE_D, STATE_B);
+
+    for (int i = 0; i < 10; ++i)
+    {
+        fsm.m_state = STATE_I;
+        s_monitor.m_last_state = STATE_I;
+        for (int j = 0; j < 1000; ++j)
+        {
+            input = randbool(1);
+            fsm.m_fi = randbool(4);
+            sprintf(s_trace, "%s%s->", s_trace, testfsm_state_to_str(fsm.m_state));
+            process(&fsm, input);
+            if (s_reset)
+            {
+                s_reset = false;
+                break;
+            }
+        }
+    }
+
+    return 0;
+}

src/storm.c

@@ -0,0 +1,133 @@
+// SPDX-License-Identifier: BSD-3-Clause
+/* STORM - State Transition Online Runtime Monitor
+ *
+ * A library for verifying correct execution order.
+ * Copyright (C) 2022 flip
+ */
+
+#include "storm.h"
+
+#include <stdlib.h>
+#include <string.h>
+#include <assert.h>
+
+#define SM_BEGIN_MAGIC  0xD00DC0FE
+#define SM_END_MAGIC    0xEF0CD00D
+
+static void sm_init(storm_sparse_matrix_t *p_this, unsigned limit);
+static unsigned *sm_get_end_magic_adr(storm_sparse_matrix_t *p_this);
+static void sm_assert_magic(storm_sparse_matrix_t *p_this);
+static bool sm_set(storm_sparse_matrix_t *p_this,
+                   const storm_state_t from,
+                   const storm_state_t to);
+static bool sm_contains(storm_sparse_matrix_t *p_this,
+                        const storm_state_t from,
+                        const storm_state_t to);
+
+
+void storm_init(storm_t *p_this,
+                storm_state_t initial,
+                const unsigned smt_size,
+                storm_violation_hook_t on_violation)
+{
+    assert(("instance must not be null", p_this != NULL));
+    
+    // initialize basic members
+    p_this->m_last_state = initial;
+    p_this->m_notify_violation = on_violation;
+    
+    // initialize sparse matrix
+    sm_init(&p_this->m_transitions, smt_size);
+}
+
+void storm_allow(storm_t *p_this,
+                 const storm_state_t current, const storm_state_t next)
+{
+    assert(("instance must not be null", p_this != NULL));
+    sm_set(&p_this->m_transitions, current, next);
+}
+
+void storm_event(storm_t *p_this, const storm_state_t new_checkpoint)
+{
+    assert(("instance must not be null", p_this != NULL));
+    
+    if (!sm_contains(&p_this->m_transitions,
+                     p_this->m_last_state, new_checkpoint))
+    {
+        if (p_this->m_notify_violation)
+        {
+            p_this->m_notify_violation(p_this->m_last_state,
+                                       new_checkpoint);
+        }
+        else
+        {
+            assert(("illegal state transition", true));
+        }
+    }
+    
+    p_this->m_last_state = new_checkpoint;
+}
+
+static void sm_init(storm_sparse_matrix_t *p_this, unsigned limit)
+{
+    assert(("instance must not be null", p_this != NULL));
+    uint32_t * p_end_magic = NULL;
+
+    p_this->m_begin_magic = SM_BEGIN_MAGIC;
+    p_this->m_limit = limit;
+    p_this->m_head = 0U;
+    memset(p_this->m_table, 0x00U, limit * sizeof(storm_transition_t));
+    
+    // set end magic
+    p_end_magic = sm_get_end_magic_adr(p_this);
+    *p_end_magic = SM_END_MAGIC;
+}
+
+static unsigned *sm_get_end_magic_adr(storm_sparse_matrix_t *p_this)
+{
+    assert(("instance must not be null", p_this != NULL));
+    uint8_t *p_magic = (uint8_t*)&(p_this->m_table);
+    p_magic += p_this->m_limit * sizeof(storm_transition_t);
+    
+    return (uint32_t*)p_magic;
+}
+
+static void sm_assert_magic(storm_sparse_matrix_t *p_this)
+{
+    const uint32_t const * p_end_magic = sm_get_end_magic_adr(p_this);
+    assert(("instance beginning magic invalid",
+           p_this->m_begin_magic == SM_BEGIN_MAGIC));
+    assert(("instance end magic invalid",
+           *p_end_magic == SM_END_MAGIC));
+}
+
+static bool sm_set(storm_sparse_matrix_t *p_this,
+                   const storm_state_t from,
+                   const storm_state_t to)
+{
+    sm_assert_magic(p_this);
+    if (p_this->m_head < p_this->m_limit)
+    {
+        p_this->m_table[p_this->m_head].m_curr = from;
+        p_this->m_table[p_this->m_head].m_next = to;
+        p_this->m_head++;
+        return true;
+    }
+    return false;
+}
+
+static bool sm_contains(storm_sparse_matrix_t *p_this,
+                        const storm_state_t from,
+                        const storm_state_t to)
+{
+    sm_assert_magic(p_this);
+    for (unsigned i = 0; i < p_this->m_head; ++i)
+    {
+        if ((p_this->m_table[i].m_curr == from) &&
+            (p_this->m_table[i].m_next == to))
+        {
+            return true;
+        }
+    }
+    return false;
+}

src/storm.h

@@ -0,0 +1,64 @@
+// SPDX-License-Identifier: BSD-3-Clause
+/* STORM - State Transition Online Runtime Monitor
+ *
+ * A library for verifying correct execution order.
+ * Copyright (C) 2022 flip
+ */
+
+#pragma once
+
+#include <stdint.h>
+#include <stdbool.h>
+
+typedef uint8_t storm_state_t;
+
+typedef struct
+{
+    storm_state_t m_curr;
+    storm_state_t m_next;
+} storm_transition_t;
+
+typedef struct
+{
+    unsigned m_begin_magic;
+    unsigned m_limit;
+    unsigned m_head;
+    storm_transition_t m_table[];
+    //m_end_magic expected here
+}
+storm_sparse_matrix_t;
+
+
+#define STORM_SM_DECL(n_limit) \
+{ \
+    unsigned m_begin_magic; \
+    unsigned m_limit; \
+    unsigned m_head; \
+    storm_transition_t m_table[n_limit]; \
+    unsigned m_end_magic; \
+}
+
+typedef void(*storm_violation_hook_t)(const storm_state_t last_checkpoint,
+                                      const storm_state_t current_checkpoint);
+
+typedef struct
+{
+    storm_state_t m_last_state;
+    storm_violation_hook_t m_notify_violation;
+    storm_sparse_matrix_t m_transitions;
+}
+storm_t;
+
+#define STORM_DECL(n_tran) \
+{ \
+    uint8_t m_last_state; \
+    struct STORM_SM_DECL(n_tran) m_stm; \
+}
+
+void storm_init(storm_t *p_this,
+                storm_state_t initial,
+                const unsigned smt_size,
+                storm_violation_hook_t on_violation);
+void storm_allow(storm_t *p_this,
+                 const storm_state_t current, const storm_state_t next);
+void storm_event(storm_t *p_this, const storm_state_t new_checkpoint);