Security-critical applications often rely on memory isolation
mechanisms to ensure integrity of critical data (e.g., keys) and
program instructions (e.g., implementing an attestation
protocol).
These include software-based security microvisor (S$\mu$V) or
hardware-based (e.g., TrustLite or SMART). Here, we must guarantee
that none of the assembly-level instructions corresponding to a
program violate the imposed memory access restrictions. We
demonstrate our approach on two architectures (S$\mu$V and
TrustLite) on which remote attestation protocols are implemented.
We extend an approach based on the Binary Analysis Platform (BAP) to
generate compiled assembly for a given C program, which is
translated to an assembly intermediate language (BIL) and ultimately
to Isabelle/HOL theories. In our extension, we develop an adversary
model and define conformance predicates imposed by an
architecture. We generate a set of programs covering all possible
cases in which an assembly-level instruction attempts to violate at
least one of the conformance predicates.
This shows that the memory access restriction of both S$\mu$V and
TrustLite are dynamically maintained. Moreover, we introduce
conformance predicates for assembly-level instructions that can
change the control flow, which improve TrustLite's memory protection
unit.