Secure Path Verification

Many embedded systems, like medical, sensing, automotive, military, require basic security functions, often referred to as "secure communications". Nowadays, interest has been growing around defining new security related properties, expressing relationships with information flow and access control. In particular, novel research works are focused on formalizing generic security requirements as propagation properties. These kinds of properties, we name them Path properties, are used to see whether it is possible to leak secure data via unexpected paths. In this paper we compare Path properties, described above, with formal security properties expressed in CTL Logic, named Taint properties. We also compare two verification techniques used to verify Path and Taint properties considering an abstraction of a Secure Embedded Architecture discussing the advantages and drawbacks of each approach.