Embedded Systems Secure Path Verification at the HW/SW Interface

Embedded systems, like medical or automotive, require basic security functions, often referred to as “secure communications”. Interest has been growing around defining and formally verifying security related properties, as potentially able to catch hard-to-detect problems. We follow novel research works focused on formalizing security requirements for information flow. We compare State Properties to Path Properties, as two approaches able to capture different aspects on how to leak/corrupt secure data via unexpected taints and paths. We also discuss tools used to verify Path and State properties, on two existing Secure Embedded Architectures, and we discuss the advantages and drawbacks of each approach.