A single malicious line of code, hidden inside a silicon chip or a software library, could lie dormant for years before silently crippling a nuclear power plant or the electricity grid. This project tackles the fundamental impossibility of testing today’s hyper-complex hardware and software systems well enough to find such hidden “backdoors” or malicious functions. Current design methods cannot guarantee that a third-party component—a pre-built “Intellectual Property Core” or a compiled software library—will behave as promised once the system is running. The researchers propose a formal “type system” that acts like a border patrol: it uses run-time checks at the boundaries of untrusted modules to intercept any intentional or accidental breach of the design specification. Static checks alone are insufficient because they cannot control behaviour after compilation. If successful, this work could make critical infrastructure—power plants, water treatment, communications networks—demonstrably more resilient to cyber attacks. It would allow engineers to trust that a system’s actual behaviour matches its design, even when using black-box components from outside suppliers. The research is fundamental in nature, developing new formal methods for system verification, but its direct application to securing safety-critical systems is immediate and concrete.
View original technical description
There are increasing concerns about the safety and security of critical infrastructure such as nuclear power plants, the electricity grid and other utilities in the face of possible cyber attacks. As ageing controllers are replaced by smart devices based on Field-Programmable Gate Arrays (FPGAs) and embedded microprocessors, the safety of such devices raises many concerns. In particular, there is the very real risk of malicious functionality hidden in the silicon or in software binaries, dormant and waiting to be activated. Current hardware and software systems are of such complexity that it is impossible to discover such malicious code through testing. We aim to address this problem by closely connecting the system design specification with the actual implementation through the use of a formal design methodology based on type systems with static and dynamic type checking. The type system will be used as a formal language to encode the design specification so that the actual implementation will automatically be checked against the specification. Static type checking of data types and multiparty session types can ensure the correctness of the interaction between the components. However, as static checking assume full access to the design source code it cannot be used to protect against potential threads issuing from third-party functional blocks (know as ``Intellectual Property Cores'' or IP cores) that are commonly used in hardware design: the provider of the IP core can claim adherence to the types and protocols, so that the IP core will meet the compile-time requirements, but the run-time the behaviour cannot be controlled using static techniques. The same applies to third-party compiled software libraries. Therefore we propose to use run-time checking of data types as well as session types at the boundaries of untrusted modules ("Border Patrol"), so that any intentional or unintentional breach of the specification will safely be intercepted.
Christian Fensch (Co-Investigator)Nobuko Yoshida (Co-Investigator)Robert Stewart (Co-Investigator)Sven-Bodo Scholz (Co-Investigator)Wim Vanderbauwhede (Principal Investigator)
Plain English summaries and category classifications on this site are generated by AI and may not perfectly reflect the original research.
Is something wrong? Let us know