Merge pull request #37 from GaloisInc/11-implement-component-mission-protection-system

11 implement component mission protection system

Author: peterohanley-galois

.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/.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

@@ -43,3 +43,16 @@ The system is connected to two temperature sensors and two fuel pressure sensors
 * V.4 MPS shall demonstrate Independence among the two trains of actuation logic (inability for the behavior of one train to interfere or adversely affect the performance another)
 * V.5 MPS shall demonstrate Completion of actuation whenever coincidence logic is satisfied or manual actuation is initiated
 * V.6 MPS shall demonstrate Independence between periodic self-test functions and trip functions (inability for the behavior of the self-testing to interfere or adversely affect the trip functions)
+
+## Porting Notes
+
+The MPS is being adapted from a high-assurance model reactor control system (HARDENS) which includes converting the Frama-C ACSL specifications to CN specifications. 
+Many C features are not yet supported by CN, the ones that most seriously affect the MPS are lack of variadic functions (all logging printfs) and lack of unions (the instrumentation_command struct).
+ACSL constructs mostly have direct analogs in CN:
+
+- `requires` and `ensures` are the same
+- `\valid` should become `Owned`, not `Block`, it requires reading and writing ability.
+- `assigns` means the value in that location can change. Other locations can be written as long as they are restored before the function exits. It doesn't make any demand on the value in the location, so it is taking and returning an `Owned`.
+- `<==>` between predicates can be replaced with `==`, it is equivalence on booleans instead of predicates.
+
+

components/mission_protection_system/README.md

@@ -0,0 +1,126 @@
+// File from: https://github.com/mpaland/printf
+///////////////////////////////////////////////////////////////////////////////
+// \author (c) Marco Paland ([email protected])
+//             2014-2019, PALANDesign Hannover, Germany
+//
+// \license The MIT License (MIT)
+//
+// Permission is hereby granted, free of charge, to any person obtaining a copy
+// of this software and associated documentation files (the "Software"), to deal
+// in the Software without restriction, including without limitation the rights
+// to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+// copies of the Software, and to permit persons to whom the Software is
+// furnished to do so, subject to the following conditions:
+// 
+// The above copyright notice and this permission notice shall be included in
+// all copies or substantial portions of the Software.
+// 
+// THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+// IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+// FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+// AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+// LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+// OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
+// THE SOFTWARE.
+//
+// \brief Tiny printf, sprintf and snprintf implementation, optimized for speed on
+//        embedded systems with a very limited resources.
+//        Use this instead of bloated standard/newlib printf.
+//        These routines are thread safe and reentrant.
+//
+///////////////////////////////////////////////////////////////////////////////
+
+#ifndef _PRINTF_H_
+#define _PRINTF_H_
+
+#include <stdarg.h>
+#include <stddef.h>
+
+
+#ifdef __cplusplus
+extern "C" {
+#endif
+
+
+/**
+ * Output a character to a custom device like UART, used by the printf() function
+ * This function is declared here only. You have to write your custom implementation somewhere
+ * \param character Character to output
+ */
+void _putchar(char character);
+
+
+/**
+ * Tiny printf implementation
+ * You have to implement _putchar if you use printf()
+ * To avoid conflicts with the regular printf() API it is overridden by macro defines
+ * and internal underscore-appended functions like printf_() are used
+ * \param format A string that specifies the format of the output
+ * \return The number of characters that are written into the array, not counting the terminating null character
+ */
+#define printf printf_
+#if !WAR_NO_VARIADICS
+int printf_(const char* format, ...);
+#endif
+
+
+/**
+ * Tiny sprintf implementation
+ * Due to security reasons (buffer overflow) YOU SHOULD CONSIDER USING (V)SNPRINTF INSTEAD!
+ * \param buffer A pointer to the buffer where to store the formatted string. MUST be big enough to store the output!
+ * \param format A string that specifies the format of the output
+ * \return The number of characters that are WRITTEN into the buffer, not counting the terminating null character
+ */
+#define sprintf sprintf_
+#if !WAR_NO_VARIADICS
+int sprintf_(char* buffer, const char* format, ...);
+#endif
+
+
+/**
+ * Tiny snprintf/vsnprintf implementation
+ * \param buffer A pointer to the buffer where to store the formatted string
+ * \param count The maximum number of characters to store in the buffer, including a terminating null character
+ * \param format A string that specifies the format of the output
+ * \param va A value identifying a variable arguments list
+ * \return The number of characters that COULD have been written into the buffer, not counting the terminating
+ *         null character. A value equal or larger than count indicates truncation. Only when the returned value
+ *         is non-negative and less than count, the string has been completely written.
+ */
+#define snprintf  snprintf_
+#define vsnprintf vsnprintf_
+#if !WAR_NO_VARIADICS
+int  snprintf_(char* buffer, size_t count, const char* format, ...);
+#endif
+int vsnprintf_(char* buffer, size_t count, const char* format, va_list va);
+
+
+/**
+ * Tiny vprintf implementation
+ * \param format A string that specifies the format of the output
+ * \param va A value identifying a variable arguments list
+ * \return The number of characters that are WRITTEN into the buffer, not counting the terminating null character
+ */
+#define vprintf vprintf_
+int vprintf_(const char* format, va_list va);
+
+
+/**
+ * printf with output function
+ * You may use this as dynamic alternative to printf() with its fixed _putchar() output
+ * \param out An output function which takes one character and an argument pointer
+ * \param arg An argument pointer for user data passed to output function
+ * \param format A string that specifies the format of the output
+ * \return The number of characters that are sent to the output function, not counting the terminating null character
+ */
+#if !WAR_NO_VARIADICS
+int fctprintf(void (*out)(char character, void* arg), void* arg, const char* format, ...);
+#endif
+
+
+#ifdef __cplusplus
+}
+#endif
+
+
+#endif  // _PRINTF_H_

components/mission_protection_system/hardware/SoC/firmware/printf.h

@@ -0,0 +1,10 @@
+#!/usr/bin/env sh
+
+cd src/components || exit 1
+
+files=( actuator.c )
+#instrumentation_common.c
+#actuation_unit.c
+#instrumentation.c
+
+cn -I ../include -I ../../hardware/SoC/firmware/ --include=../include/wars.h "${files[@]}"

components/mission_protection_system/run_cn_proofs.sh

@@ -0,0 +1,6 @@
+#! /usr/bin/env bash
+set -e
+
+sudo docker run -v ${PWD}:/HARDENS -it \
+    framac/frama-c:dev \
+    make -C /HARDENS/src -f frama_c.mk