Authors: Aljosa Pasic and Marco Roveri
A manifesto is a name usually given to a public declaration of beliefs, principles, and intentions, often issued by a group or individual, proposing specific actions or policies. The most famous and influential manifestos in history are probably the Communist Manifesto by Karl Marx and Friedrich Engels and the Declaration of Independence by Thomas Jefferson, both being embraced by two very different political and ideological systems.
Less frequently, manifestos are also associated with software components and specifications, created by groups of software developers or professionals less known than those mentioned above. Examples include the Agile Manifesto, which emphasizes flexibility in development, the DevOps Manifesto, which focuses on collaboration between previously separated teams, and the Serverless Manifesto, which promotes the use of serverless computing architectures.
Within the CROSSCON Internet of Things (IoT) security stack, each component should be modular, reusable, interoperable, and well-documented. We also believe that they should come with a “Formal Certification Manifesto” so that these components can be easily re-verified after being shared, reused, or integrated. Although Open-Source Software (OSS) communities have existed for many years, Open-Source Hardware (OSH) is much less known. Among many OSH ecosystems, RISC-V is the most relevant one for CROSSCON. It revolves around an instruction set architecture for microprocessor cores, originally developed at the University of California at Berkeley and released under an open-source license. RISC-V processors are used in a wide range of contexts, including IoT, general purpose operating systems like Linux, supercomputing, and automotive technologies. Currently, there are over 100 RISC-V cores available in various semiconductor types, and they are supported by different RTOS. While this ecosystem and CROSSCON positioning will be discussed in more in detail in the exploitation activities of the project, they also face challenges on their own. Verification, for example, is costly and sometimes represents a bottleneck in the RISC-V design cycle.
One of the core tasks in CROSSCON is to openly design a security stack for connected devices and IoT, considering the requirements for enabling formal verification of security properties such as memory isolation and secure storage, as well as the life-time operations, including bug fixing, cross-compilation, and updates/patches. This CROSSCON specification will be presented in a “Formal Certification Manifesto” associated with each element of the stack, including access policies, assumptions, used resources, and behaviors, among other information, formulated with suitable formalisms such as first-order formulas complemented with temporal logic formulas. This manifesto will then be the primary enabler for other activities, such as the formal verification of different components, continuous verification of patches, and security updates, among others.
This work leverages existing specifications, e.g., the RISC-V formal verification framework, complementing these with suitable extensions. Therefore, we will explain the importance of RISC-V and its relevance to the CROSSCON project.