Changes in stubs and linker.py for Authentic Execution

src/drivers/linker.py

@@ -17,6 +17,7 @@
 
 MAC_SIZE = int(sancus.config.SECURITY / 8)
 KEY_SIZE = MAC_SIZE
+CONNECTION_STRUCT_SIZE = 6 + KEY_SIZE
 
 
 class SmEntry:
@@ -63,7 +64,7 @@ def add_sym(file, sym_map):
 
     args += [file, file]
     call_prog('msp430-elf-objcopy', args)
-    return file 
+    return file
 
 
 def parse_size(val):
@@ -92,18 +93,23 @@ def get_symbol(elf_file, name):
 
 def get_io_sym_map(sm_name):
     sym_map = {
-        '__sm_handle_input':    '__sm_{}_handle_input'.format(sm_name),
-        '__sm_num_inputs':      '__sm_{}_num_inputs'.format(sm_name),
-        '__sm_num_connections': '__sm_{}_num_connections'.format(sm_name),
-        '__sm_io_keys':         '__sm_{}_io_keys'.format(sm_name),
-        '__sm_input_callbacks': '__sm_{}_input_callbacks'.format(sm_name),
-        '__sm_output_nonce':    '__sm_{}_output_nonce'.format(sm_name),
-        '__sm_send_output':     '__sm_{}_send_output'.format(sm_name),
-        '__sm_set_key':         '__sm_{}_set_key'.format(sm_name),
-        '__sm_X_exit':          '__sm_{}_exit'.format(sm_name),
-        '__sm_X_stub_malloc':   '__sm_{}_stub_malloc'.format(sm_name),
+        '__sm_handle_input':        '__sm_{}_handle_input'.format(sm_name),
+        '__sm_num_inputs':          '__sm_{}_num_inputs'.format(sm_name),
+        '__sm_num_connections':     '__sm_{}_num_connections'.format(sm_name),
+        '__sm_max_connections':     '__sm_{}_max_connections'.format(sm_name),
+        '__sm_io_connections':      '__sm_{}_io_connections'.format(sm_name),
+        '__sm_input_callbacks':     '__sm_{}_input_callbacks'.format(sm_name),
+        '__sm_send_output':         '__sm_{}_send_output'.format(sm_name),
+        '__sm_set_key':             '__sm_{}_set_key'.format(sm_name),
+        '__sm_attest':              '__sm_{}_attest'.format(sm_name),
+        '__sm_X_exit':              '__sm_{}_exit'.format(sm_name),
+        '__sm_X_stub_malloc':       '__sm_{}_stub_malloc'.format(sm_name),
         '__sm_X_stub_reactive_handle_output':
-            '__sm_{}_stub_reactive_handle_output'.format(sm_name)
+            '__sm_{}_stub_reactive_handle_output'.format(sm_name),
+        '__sm_X_public_start':      '__sm_{}_public_start'.format(sm_name),
+        '__sm_X_public_end':        '__sm_{}_public_end'.format(sm_name),
+        '__sm_X_secret_start':      '__sm_{}_secret_start'.format(sm_name),
+        '__sm_X_secret_end':        '__sm_{}_secret_end'.format(sm_name)
     }
 
     return sym_map
@@ -115,7 +121,7 @@ def get_io_sect_map(sm_name):
         '.rela.sm.X.text':  '.rela.sm.{}.text'.format(sm_name),
     }
 
-    for entry in ('__sm{}_set_key', '__sm{}_handle_input'):
+    for entry in ('__sm{}_set_key', '__sm{}_attest', '__sm{}_handle_input'):
         map['.sm.X.{}.table'.format(entry.format(''))] = \
             '.sm.{}.{}.table'.format(sm_name, entry.format('_' + sm_name))
         map['.rela.sm.X.{}.table'.format(entry.format(''))] = \
@@ -136,15 +142,19 @@ def create_io_stub(sm, stub):
 
 
 def sort_entries(entries):
-    # If the set_key entry exists, it should have index 0 and if the
-    # handle_input entry exists, it should have index 1. This is accomplished by
-    # mapping those entries to __ and ___ respectively since those come
+    # If the set_key entry exists, it should have index 0, if the
+    # attest entry exists, it should have index 1 and if
+    # handle_input entry exists, it should have index 2. This is accomplished by
+    # mapping those entries to __, ___ and ___ respectively since those come
     # alphabetically before any valid entry name.
     def sort_key(entry):
         if re.match(r'__sm_\w+_set_key', entry.name):
             return '__'
-        if re.match(r'__sm_\w+_handle_input', entry.name):
+        if re.match(r'__sm_\w+_attest', entry.name):
             return '___'
+        if re.match(r'__sm_\w+_handle_input', entry.name):
+            return '____'
+
         return entry.name
 
     entries.sort(key=sort_key)
@@ -212,7 +222,7 @@ def sort_key(entry):
     for a in archive_files:
         debug("Unpacking archive for Sancus SM inspection: " + a)
         file_name = a
-        if ':' in a: 
+        if ':' in a:
             # support calls such as -lib:/full/path
             file_name = file_name.split(':')[1]
 
@@ -269,6 +279,7 @@ def sort_key(entry):
 elf_relocations = defaultdict(list)
 
 added_set_key_stub = False
+added_attest_stub = False
 added_input_stub = False
 added_output_stub = False
 
@@ -409,6 +420,14 @@ def sort_key(entry):
                         input_files_to_scan.append(generated_file)
                         added_set_key_stub = True
 
+                    if not added_attest_stub:
+                        # Generate the attest stub file
+                        generated_file = create_io_stub(sm, 'sm_attest.o')
+                        generated_object_files.append(generated_file)
+                        # And register it to also be scanned by this loop later
+                        input_files_to_scan.append(generated_file)
+                        added_attest_stub = True
+
                     if which == 'input':
                         dest = sms_inputs
 
@@ -463,7 +482,7 @@ def sort_key(entry):
 The YAML file allows to set the following things:
   1) warn whenever an ocall is performed and abort linking process
   2) Swap out assembly stubs for custom project dependent values
-  3) Set a peripheral offset for the first SM to 
+  3) Set a peripheral offset for the first SM to
 """
 try:
     file_path = ''
@@ -829,24 +848,36 @@ def sort_key(entry):
 
         call_prog('msp430-gcc', ['-c', '-o', o_file, c_file])
 
-        input_callbacks += '    {}(.sm.{}.callbacks)\n'.format(o_file, sm)
+        input_callbacks += '    KEEP({}(.sm.{}.callbacks))\n'.format(o_file, sm)
         input_callbacks += '    . = ALIGN(2);'
 
-    # Table of connection keys
-    io_keys = ''
+    """
+    Table of connections: in a reactive application, a connection links the
+    output of a SM (defined using the macro `SM_OUTPUT`) to the input of another
+    (defined using the macro `SM_INPUT`).
+    These connections are stored in a `Connection` array on each SM (see
+    `reactive_stubs_support.h`). The array is allocated here with a fixed size,
+    according to the `num_connections` parameter in the SM config (default 0).
+    """
 
-    if len(ios) > 0:
-        io_keys += '__sm_{}_io_keys = .;\n'.format(sm)
-        io_keys += '    . += {};\n'.format(len(ios) * KEY_SIZE)
-        io_keys += '    . = ALIGN(2);'
+    num_connections = ''
+    io_connections = ''
+
+    if hasattr(sm_config[sm], "num_connections"):
+        sm_num_connections = sm_config[sm].num_connections
+    else:
+        sm_num_connections = 0
 
-    # Nonce used by outputs
-    outputs_nonce = ''
+    if len(ios) > 0:
+        # make sure we allocate space even if num_connections is zero
+        io_connections_size = max(sm_num_connections * CONNECTION_STRUCT_SIZE, 2)
 
-    if len(outputs) > 0:
-        outputs_nonce += '__sm_{}_output_nonce = .;\n'.format(sm)
-        outputs_nonce += '    . += 2;\n'
-        outputs_nonce += '    . = ALIGN(2);'
+        num_connections += '__sm_{}_num_connections = .;\n'.format(sm)
+        num_connections += '    . += 2;\n'
+        num_connections += '    . = ALIGN(2);'
+        io_connections += '__sm_{}_io_connections = .;\n'.format(sm)
+        io_connections += '    . += {};\n'.format(io_connections_size)
+        io_connections += '    . = ALIGN(2);'
 
     # Set data section offset if peripheral access is set
     # in that case, optionally provide first SM with exclusive access to last peripheral
@@ -859,10 +890,10 @@ def sort_key(entry):
                                              exit_file, '\n    '.join(tables),
                                              input_callbacks,
                                              '\n    '.join(extra_labels)))
-    
+
     data_sections.append(data_section.format(sm, '\n    '.join(id_syms),
-                                             args.sm_stack_size, io_keys,
-                                             outputs_nonce,
+                                             args.sm_stack_size, num_connections,
+                                             io_connections,
                                              data_section_start))
 
     if sm in sms_entries:
@@ -880,7 +911,7 @@ def sort_key(entry):
         symbols.append('__sm_{}_io_{}_idx = {};'.format(sm, io, index))
 
     # Add symbols for the number of connections/inputs
-    symbols.append('__sm_{}_num_connections = {};'.format(sm, len(ios)))
+    symbols.append('__sm_{}_max_connections = {};'.format(sm, sm_num_connections))
     symbols.append('__sm_{}_num_inputs = {};'.format(sm, len(inputs)))
 
     if args.prepare_for_sm_text_section_wrapping:

src/drivers/sancus/sancus_config.py

@@ -12,6 +12,7 @@
 SM_CONFIG_DEFAULT_SM_EXIT=""
 SM_CONFIG_DEFAULT_SM_ISR=""
 SM_CONFIG_DEFAULT_PERIPHERAL_OFFSET=0
+SM_CONFIG_DEFAULT_NUM_CONNECTIONS=None
 
 class SmParserError(Exception):
     """ 
@@ -125,6 +126,7 @@ def _safe_config_parse(name, default_val):
         self._sm_exit  = _safe_config_parse('sm_exit',  SM_CONFIG_DEFAULT_SM_EXIT)
         self._sm_isr   = _safe_config_parse('sm_isr' ,  SM_CONFIG_DEFAULT_SM_ISR)
         self._peripheral_offset = _safe_config_parse('peripheral_offset', 0)
+        self._num_connections = _safe_config_parse('num_connections', SM_CONFIG_DEFAULT_NUM_CONNECTIONS)
 
     """
     Getters as properties for all class variables.
@@ -178,6 +180,13 @@ def peripheral_offset(self):
         else:
             raise AttributeError
 
+    @property
+    def num_connections(self):
+        if self._num_connections != SM_CONFIG_DEFAULT_NUM_CONNECTIONS:
+            return abs(self._num_connections)
+        else:
+            raise AttributeError
+
     def __str__(self):
         if self._contains_config:
             s = '' + self._name + ':\n'
@@ -187,6 +196,7 @@ def __str__(self):
             if hasattr(self, 'sm_exit'): s += '\t\t SM_EXIT: ' + self._sm_exit  + '\n'
             if hasattr(self, 'sm_isr'): s += '\t\t SM_ISR: ' + self._sm_isr  + '\n'
             if hasattr(self, 'peripheral_offset'): s += '\t\t Peripheral Offset: ' + str(self._peripheral_offset)  + '\n'
+            if hasattr(self, 'num_connections'): s += '\t\t Number of connections: ' + str(self._num_connections)  + '\n'
         else:
             s = 'No YAML config provided.'
         return s

src/drivers/sm-config-example.yaml

@@ -23,6 +23,13 @@ my_sm_1:
     # amount of byte. This allows to map the data section over the
     # peripherals to grant exclusive and faster access to these peripherals
     - peripheral_offset: 159
+    # Set the maximum number of connections allowed for this SM in a reactive
+    # application. Connections link the output of a SM (defined using the macro
+    # `SM_OUTPUT`) with the input of another (defined using the macro
+    # `SM_INPUT`). If this SM does not have any inputs nor outputs, there is no
+    # need to specify this parameter (default value is zero). In the Authentic
+    # Execution framework, this parameter is automatically configured.
+    - num_connections: 3
 my_sm_2:
  	- disallow_outcalls: True
 

src/sancus_support/reactive.h

@@ -6,19 +6,20 @@
 #include <stdint.h>
 
 typedef uint16_t io_index;
+typedef uint16_t conn_index;
 typedef uint8_t  io_data __attribute__((aligned(2)));
 
 // The ASM symbols are used for the linker to be able to detect inputs/outputs
 
-#define SM_OUTPUT_AUX(sm, name)                                         \
-    asm("__sm_" #sm "_output_tag_" #name " = 0\n");                     \
-    SM_FUNC(sm) void name(const io_data* data, size_t len)              \
-    {                                                                   \
-        extern char __sm_##sm##_io_##name##_idx;                        \
-        SM_FUNC(sm) void __sm_##sm##_send_output(unsigned int,          \
-                                                 const void*, size_t);  \
-        __sm_##sm##_send_output((io_index)&__sm_##sm##_io_##name##_idx, \
-                                data, len);                             \
+#define SM_OUTPUT_AUX(sm, name)                                                \
+    asm("__sm_" #sm "_output_tag_" #name " = 0\n");                            \
+    SM_FUNC(sm) uint16_t name(const io_data* data, size_t len)                 \
+    {                                                                          \
+        extern char __sm_##sm##_io_##name##_idx;                               \
+        SM_FUNC(sm) uint16_t __sm_##sm##_send_output(unsigned int,             \
+                                                 const void*, size_t);         \
+        return __sm_##sm##_send_output((io_index)&__sm_##sm##_io_##name##_idx, \
+                                data, len);                                    \
     }
 
 #define SM_OUTPUT(sm, name) SM_OUTPUT_AUX(sm, name)

src/sancus_support/sm_support.h

@@ -4,6 +4,7 @@
 #include "config.h"
 
 #include <stddef.h>
+#include <stdint.h>
 
 #if __GNUC__ >= 5 || __clang_major__ >= 5
 
@@ -199,15 +200,12 @@ extern char __unprotected_sp;
 
 #endif
 
-#define __OUTSIDE_SM( p, sm )                                                  \
-    ( ((void*) p < (void*) &__PS(sm)) || ((void*) p >= (void*) &__PE(sm)) ) && \
-    ( ((void*) p < (void*) &__SS(sm)) || ((void*) p >= (void*) &__SE(sm)) )
-
 /*
  * Returns true iff whole buffer [p,p+len-1] is outside of the sm SancusModule
  */
-#define sancus_is_outside_sm( sm, p, len) \
-    ( __OUTSIDE_SM(p, sm) && __OUTSIDE_SM((p+len-1), sm) )
+#define sancus_is_outside_sm(sm, p, len) \
+    ( is_buffer_outside_region(&__PS(sm), &__PE(sm), p, len) && \
+      is_buffer_outside_region(&__SS(sm), &__SE(sm), p, len) )
 
 /**
  * Interrupt vector for the Sancus violation ISR.
@@ -311,6 +309,37 @@ sm_id sancus_enable_wrapped(struct SancusModule* sm, unsigned nonce, void* tag);
 #undef always_inline
 #define always_inline static inline __attribute__((always_inline))
 
+/*
+ * Returns true if buf is outside the memory region [start, end)
+ * if start >= end, immediately return false
+ */
+always_inline int is_buffer_outside_region(void *start_p, void *end_p,
+    void *buf_p, size_t len) {
+  uintptr_t start = (uintptr_t) start_p;
+  uintptr_t end   = (uintptr_t) end_p;
+  uintptr_t buf   = (uintptr_t) buf_p;
+  uintptr_t buf_end;
+
+  // make sure start < end, otherwise return false
+  if (start >= end) {
+    return 0;
+  }
+
+  if(len > 0) {
+    buf_end = buf + len - 1;
+  }
+  else {
+    buf_end = buf;
+  }
+
+  /* check for int overflow and finally validate `buf` falls outside */ 
+  if( (buf <= buf_end) && ((end <= buf) || (start > buf_end))) {
+    return 1;
+  }
+
+  return 0;
+}
+
 /**
  * Performs constant time comparison between to buffers
  * Returns 0 if the first `n` bytes of the two buffers are equal, -1 otherwise

src/stubs/CMakeLists.txt

@@ -23,6 +23,7 @@ set(EXTRA_FLAGS -I${CMAKE_SOURCE_DIR}/src/sancus_support)
 add_object(sm_output.o sm_output.c ${EXTRA_FLAGS})
 add_object(sm_input.o sm_input.c ${EXTRA_FLAGS})
 add_object(sm_set_key.o sm_set_key.c ${EXTRA_FLAGS})
+add_object(sm_attest.o sm_attest.c ${EXTRA_FLAGS})
 
 set(STUBS
     ${CMAKE_CURRENT_BINARY_DIR}/sm_entry.o
@@ -34,6 +35,7 @@ set(STUBS
     ${CMAKE_CURRENT_BINARY_DIR}/sm_output.o
     ${CMAKE_CURRENT_BINARY_DIR}/sm_input.o
     ${CMAKE_CURRENT_BINARY_DIR}/sm_set_key.o
+    ${CMAKE_CURRENT_BINARY_DIR}/sm_attest.o
     ${CMAKE_CURRENT_BINARY_DIR}/sm_mmio_entry.o
     ${CMAKE_CURRENT_BINARY_DIR}/sm_mmio_exclusive.o