| Abstract: |
Adding new devices to OT or critical infrastructure network can be tenuous. The nature of a typical OT installation does not allow for much variance in network traffic: networks are relatively static and the devices on these networks are notoriously fragile. However, the growing interconnectedness of OT networks introduces a greater need for cyber security measures and appliances to counteract the larger attack surface. When you are designing a new device for your control network, you need to understand both your needs and solution as much as possible to minimize the chance of errant, or even malicious, network traffic wreaking havoc. The SeL4 microkernel offers formally verified primitives for building secure native applications to leverage its already robust security properties. Modeling these primitives in TLA+ allows a pipeline to be built from the OT device specification stage to the deployment stage that maintains modeled and checked security properties to the final product. This work presents the novel models of two inter-process communication primitives: dataports and event notifications. These primitives are modeled within TLA+ and used withing a proof of concept specification that translates the TLA+ specification into a CAmkES architecture for a toy OT device. |