Laot - man in the middle defence for critical infrastructure

"seL4 is a high-assurance, high-performance operating system microkernel. It is unique because of its comprehensive formal verification, without compromising performance. It is meant to be used as a trustworthy foundation for building safety and security-critical systems." - sel4.systems.

The Laot project uses the seL4 microkernel in order to provide:

Mission: build a provably secure device in order to protect critical infrastructure and legacy systems using seL4 and formal methods.

The Anti-FAQ: why not may be of use in describing the problems laot is intended to answer, but critical Infrastructure such as power systems remains vulnerable to both advanced attacks and accident since:

Legacy systems: devices and OS are often unsupported.
Current systems: are also large which means they will have errors (20M SLOC x 1 error per 1000 SLOC = 20000 errors).
Communications infrastructure remains vulnerable.
The seL4 micro kernel provides the secure base with isolated components
Laot provides policy based protocol protection, e.g. outside system may be prevented from updating parameters such as voltage setpoints.

The project is in final prototyping stage but comments are welcome, see Forum or contact the team members, see Who directly. Interested parties are welome to contact any of the team members.

Laot: the device in the middle

The device itself is a small two port ethernet which provides protection and monitoring. It does not require changes to existing infrastructure or legacy systems.

# top level context for laot
scale=1.0
boxrad = 10px

Main: [
 ellipse  "Network" "IoT..." "SCADA" fit dashed fill 0xD0B0B0
 line <-> "Ethernet" above "Outside" below
 box "Laot" "Filter" "Fix/Find" fit
 line <-> "Ethernet" above "Inside" below
 ellipse "Device" "Under" "Protection" dashed fit fill 0x00B000 
]

Watchers: [
 box "History" "Versions, Logs" "Append Only" fit
 line ->
 box "Operator" "What has changed?" "Why? How to make it safe!" dashed fit fill 0xF0F0F0
] with .n at Main.Laot.s -(0.0, 0.5)

line <-> from Main.Laot.s to Watchers.Operator.n
arrow from Main.Laot.s to Watchers.History.n

The device allows us to:

Limit what gets from the outside to the inside, e.g. "Only accept start/stop commands every 30 minutes"
Transparent: allow the operator to select a transparent mode which doesn't filter for updates.
Compare and difference system states, e.g. "What parameters have been changed from the as commissioned values?"
Automatic or manual reversion to previous safe states, e.g. "On Darwin Grid black: disable PV for two hours"

Laot Internals

The key point is that each of the components is isolated by seL4 which means:

Each Checker cannot effect later steps other than by changing its output. For example the Limiter below could be a IEC61131 program and even if it was compromised the Final Safety Checks would still completed.
The Watchers only have read access to the state and provide visibility to Operations.
The Recorder is an append only blockchain system that provides version control and checkpointing. For example Operations can see the changes to parameters from 2020-4-1 to today and revert them if required. This is a very good idea (TM).

# top level context for laot
scale=0.7
boxrad = 10px
down

Main: [
  "Checkers (each isolated)" bold
  ellipse "Network" "IoT, SCADA" fit dashed fill 0xD0B0B0
  line  <-> "Ethernet" above aligned "Outside" below aligned 
  box "Outsider" "Protocols..." fit fill 0xD0B0B0
  line <-> "State" above aligned
  box "Limiter" "Limits on Values,..." fit fill 0x85B00B
  line <-> "State" above aligned
  box "Checker" "Final Safety Checks" fit fill 0x05D000
  line <-> "State" above aligned
  box "Insider" "Protocols..." fit fill 0x00D000
  line <-> "Ethernet" above aligned "Inside" below aligned
  ellipse "Device" "Under" "Protection" dashed fit fill 0x20C020
]

Watchers: [
  "Watchers(read only)" bold
  cylinder "Logger" "Whats happened" width 130% height 130% fit fill 0xC0C0E0
  move
  box "View" "Whats happening" fit fill 0xC0C0E0
  move
  cylinder "History" "Wavy lines" height 130% fit fill 0xC0C0E0
] with .n at Main.Limiter.s + (2.5, 1.0)

Operations: [
  "Operations" bold
  box "Operator" fill 0x909000
  move 4
  cylinder "Recorder" "OpenBSD not seL4" "Blockchain, Append Only+Version Control" italic fit width 120% height 130% fill 0x3090FF
] with .n at Main.Limiter.s + (4.5, 2.5)

line -> from Main.Outsider.e to Watchers.Logger.w 
line -> from Main.Limiter.e to Watchers.Logger.w
line -> from Main.Checker.e to Watchers.Logger.w
line -> from Main.Insider.e to Watchers.Logger.w


line -> from Main.Outsider.e to Watchers.View.w
line -> from Main.Limiter.e to Watchers.View.w
line -> from Main.Checker.e to Watchers.View.w
line -> from Main.Insider.e to Watchers.View.w

line -> from Main.Outsider.e to Watchers.History.w
line -> from Main.Limiter.e to Watchers.History.w
line -> from Main.Checker.e to Watchers.History.w
line -> from Main.Insider.e to Watchers.History.w

line <-> from Main.Network.e to Operations.Operator.w "existing systems" above aligned bold "no change" below bold aligned
line -> from Watchers.Logger.e to Operations.Operator.s "https:" above aligned
line -> from Watchers.View.e to Operations.Operator.s "https:" above aligned
line -> from Watchers.History.e to Operations.Operator.s "https:" above aligned

line -> from Watchers.Logger.e to Operations.Recorder.n "https:+" above aligned
line -> from Watchers.View.e to Operations.Recorder.n "https:+" above aligned
line -> from Watchers.History.e to Operations.Recorder.n "https:+" above aligned

line -> from Operations.Operator.s to Operations.Recorder.n "https:" above aligned

The gentle reader should perhaps note that the diagrams simplifies the data flow, it flows down via one path and returns by a separate one, which could have different checks, still the diagram is close.

Simple data model and configuration

Laot is configured using a simple name and property model so that the system can be configured via a spreadsheet. For example:

name   ... -limit_min -limit_max  -ensure  -units....
P           100       200                  kW
Q      ...                        Q >= 0   kvar

This representation is then compiled on the laot device itself has the benefits of:

Simplify configuration: there are no custom tools required.
Preventing attacks via engineering workstations.
To translate into security speak: "The trusted computing base is on the device".

Formal methods: state, checks and steps

Laot uses formal methods in both seL4 and in its checks and limits. It follows the well known TLA+, Z and B methods all of which have been used extensively in life critical systems. The systems lets us write relatively simple requirements such as:

 100 <= P and P <= 200     # limit value for P
 P' > P                    # new/output value for P' is more than old/input
 P' == P@"as-commissioned" # historical values name
 dP = P - P@-60s           # relative time access dP change overlast 60s
 Q@2020-04-01              # absolute time

The intent is to provide simple way to capture and test real time requirements.

Summary

Loat can provide a significant improvement to our existing infrastructure including protecting legacy devices from either deliberate or accidental failures.