System and method for formal modelling of trusted edge IoT security gateways

Inventors

Vasudevan, Amit • McCORMACK, Matthew • Sekar, Vyas

Abstract

Disclosed herein is a method for defining a model of a trusted IoT security gateway architecture based on a microhypervisor, wherein evaluation of the model provides a guarantee that the correct security protections are applied to each IoT device's network traffic at all times, including when under attack. The models defined in accordance with the method disclosed herein are used to verify security gateway architectures that provide robust trust properties to a broad range of legacy hardware platforms utilizing existing software with a reasonable performance overhead.

Core Innovation

The invention describes a method for verifying a trusted gateway for IoT devices by creating a model of the trusted gateway and evaluating security properties using a mathematical logic solver. A controller defining a control plane is defined in a modelling language, where the controller executes software that is either protected by or attested by a controller microhypervisor, and a security gateway defining a data plane is also defined in the modelling language, where the data plane is attested by a security gateway microhypervisor.

The method compiles the model into a mathematical logic problem and evaluates the model using a mathematical logic solver. The model includes a function specifying how data packets sent to and received from an IoT device are processed at the security gateway, including sending a packet to a vSwitch for routing to a specific middlebox that determines if the packet is benign or malicious.

The model further includes a predicate with constraints that must be satisfied to establish the trusted gateway, including preventing an attacker from tampering with policies of the controller, ensuring a secure control channel immune to an attacker injecting malicious messages, requiring correct software to be running on the controller, vSwitch and each middlebox, and requiring that each packet follow a path specified by the controller and enforced by the vSwitch and each middlebox. The model includes an assert interface comprising one or more statements that must evaluate as true and providing counterexamples if any statement does not evaluate as true.

Evaluating the model using the logic solver therefore verifies that the trusted gateway satisfies the asserted trust properties, and counterexamples can be produced when the overarching trust property is not satisfied under the constraints. The disclosed approach is applied to the formal modelling and verification of a controller-plus-gateway architecture for trusted edge IoT security gateways built on a microhypervisor.

Claims Coverage

Independent claim clm-00001 covers the end-to-end method with 5 inventive features: modelling a controller and a security gateway, compiling to a mathematical logic problem, evaluating with a mathematical logic solver, using an assert interface, and applying trust constraints with packet-processing and path enforcement.

The independent claim centers on formal modelling of a controller microhypervisor-protected or attested control plane and a security gateway microhypervisor-attested data plane, compilation to a mathematical logic problem, and solver-based evaluation using an assert interface. The claim further requires controller policy protection, a secure control channel, correct software on controller, vSwitch and middleboxes, and controller-specified packet paths enforced by the vSwitch and middleboxes, with counterexamples produced when assertions fail.

Stated Advantages

Documented Applications