d-GUARD: Thwarting Denial-of-Service Attacks via Hardware Monitoring of Information Flow using Language Semantics in Embedded Systems

As low-level embedded systems are vulnerable to attacks that exploit flaws in either hardware or software, it is essential to enforce secure policies to protect the system from malicious instructions that significantly alter program behavior. To improve efficiency of implementation, high-level secure policy languages have been defined such that the policies can be directly synthesized into hardware monitors. However, the language semantics define policies that are static throughout the program execution which limits the flexibility. Moreover, secure policies target processor pipelines and not the network-on-chip (NoC) connecting several processor where denial-of-service attacks could originate. In this paper, we enable dynamically reconfigurable security policies through a high-level language called D-GUARD that target both processor pipeline and NoC architecture in mutlicore embedded systems. Alongside static policies, D-GUARD’s semantics support policies that dynamically change behavior in response to program conditions at runtime. In addition, we also propose policies to thwart denial-of-service attacks by rate limiting the packet flow into the network using the same dynamic policies expressed by D-GUARD. We describe a Verilog compiler to support realizing policies as hardware monitors for both processor pipelines and network interfaces. D-GUARD 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.