Without the isolation abstractions of operating systems, low-level embedded systems are especially vulnerable to attacks that exploit flaws in either software or hardware to gain control of program behavior. Runtime monitors at the hardware level have shown promise towards by identifying malicious instructions and enforcing programmer-defined policy at runtime. However, the efficiency of monitors comes at the cost of ease of implementation, as policies for ensuring the safe execution of software must be defined at the hardware level. To bridge the abstraction gap, high-level security policy languages have been defined with the ability to be synthesized into hardware monitors, but are limited by semantics that only define policies whose behavior remains static throughout a program's execution, which limits the practical use case.
In this paper, we enable dynamically reconfigurable security policies through a high-level language named DAGGER. Alongside static policies, DAGGER's semantics support policies that dynamically change behavior in response to expert-defined conditions at runtime. Additionally, we introduce a Verilog compiler to support realizing policies as hardware monitors. DAGGER is developed using the Coq proof assistant, enabling the formal verification of policy correctness and other properties. This approach takes advantage of the abstractions and expressiveness of a higher-level language while minimizing the overhead that comes with other general-purpose approaches implemented purely in hardware, as well as offering the groundwork for a formally verified tool chain.