The global logical address space
One of Kirsch’s central design paradigms is the global logical address space, or GLAS. The GLAS allows all contexts in a system to agree on the semantics of GLAS addresses. Each address in the GLAS corresponds to a unique resource present of the SoC. Therefore, each context sees a subset of the GLAS.
However, hardware addresses can be (and are sometimes) aliased, and we require that all resources are uniquely placed the GLAS. At least one of the two resources has to be placed at a different address in the GLAS than it appears at on the physical interconnect.
Why is it useful?
The GLAS is a solid foundation that we can build Kirsch on top of. Having ensured that all contexts in a system agree on the semantics of all addresses, we can treat the contexts that anything running on top of run in as a unified global context, which greatly simplifies both programming and reasoning about security.
Who has tried this before?
Why retry it now?
Deriving the GLAS
Given a decoding net that describes a platform, our goal is to derive the GLAS from the views of the individual contexts. We encode our problem as in the smtlib2 format.
Our encoding consists of two steps: first, we obtain a flattened address space representation for every context and resource in the system. For each of the resource ranges r accessible by a context c, we define a variable that represents the offset between r’s location in the GLAS and where it appears for c.
For each of the unique resource ranges, we then insert disjointness constraints, ensuring that two ranges cannot overlap. A brief overview of the constraints can be seen below.
; Declare one variable for each address range a resource shows up in a
; specific context c
;
; Introduces at most #c * #r variables
(declare-const co_<c>_<r_offset> Int)
; Declare one variable for each resource range r in the GLAS
;
; Introduces at exactly #r variables
(declare-const go_<r>_<r_offset> Int)
; Assert that co must be the offset applied to r in ctx to get the offset
;
; Introduces at most #c * #r constraints
(assert (= (+ offset(c, r) co_<c>_<r_offset>) go_<r>_<r_offset>))
; Assert that the ranges for two resources r1 and r2 cannot overlap
;
; Introduces (#r)^2 constraints <-- potentially expensive
(assert (or
(<= r1_end r2_start)
(<= r2_end r1_start)))
However, our encoding does not have a preferred solution yet. We would like to prefer solutions that avoid placing resources at non-zero offsets, and thus we introduce some soft constraints.
; Find a solution that minimizes the amount of shifting overall.
;
; Adds at most #c * #r soft constraints;
(assert-soft (= co_<c>_<r_offset> 0))
Furthermore, we might also need some hard constraints. One example where these come up is during MMU initialization: one possible implementation maps a portion of memory 1-1 between the GLAS and the physical address space, so that after enabling the MMU, execution continues succesfully.
(assert (<arbitrary expressions>))
However, arbitrary constraints can easily lead to a situation where resources must be placed overlapping in the GLAS, so we have to be careful.
Optimization opportunities
Our current encoding is the result of a naive encoding of the problem. There are some avenues for improvement, both for derivation speed and output quality.
Speed: use n-bit bitvectors instead of integers. Can we encode the optimziation criteria differently, and e.g. use binary search to determine a solution?
Quality: adjust optimization criteria. Currently, we assume that having to offset accesses to variables is equally bad for each context. However, different contexts pay different costs: contexts with an MMU could virtualize the GLAS at a much lower cost, and cope with non-zero offsets for little cost. Figuring out other criteria, and how to encode them, also sounds interesting.