Security Analysis of Automotive Architectures using Probabilistic Model Checking


In this work, we are looking at how to analyze automotive architectures using methods from the domain of probabilistic model-checking. We assess components separately and for their exploitability and patchability and combine these assessments with a given architecture into a continuous-time Markov chain. This Markov chain can be analyzed for properties such as "How long is message m exploitable within 1 year?". The results give us a quantifiable measure for the security of an automotive architecture and allows us to compare architectures.

Here you can find my paper and presentation, as presented on the 52nd Design Automation Conference (DAC) 2015 in San Francisco.