Formal Analysis of the I-ETMS Train Control Systems Safety Cases

Modern trains are computer networks on wheels that receive encrypted commands from backend servers. Rail is an important part of critical national infrastructure; many supermarkets rely on rail to stock the shelves with food and many employees need functioning trains to get to work. This makes both the safety and the cyber security of rail interesting to study. In this talk I will discuss how cyber security formal verification methods can be used to analyse system safety. I will present our analysis of the closed source, proprietary I-ETMS train control system; we first go from public safety case documents to formal, cyber security models in the Tamarin checker. We then look at how safety risks can be encoded in Tamarin and use the tool to look for cyber attacks that may lead to safety case failures.git