Langsec in Pectore
A secure pacemaker created from formal grammars
Design and build a Proof-of-Concept (PoC) cardiac pacemaker circuit with an analog/mixed-signal CMOS ASIC based on a description of the device functionality as formal grammar/automaton based on language security (langsec) design principles. Internet-of-things (IoT) devices are usually designed around a general purpose microcontroller with a much larger state space than needed for their purpose. Only after the initial design, interface capabilities of the IoT device are artificially restricted for privacy and security. An implanted pacemaker is a safety-critical IoT device that fits into a very small state space, as proven by early pacemaker designs that did not use high performance microcontrollers. Langsec methods use formal grammars to specify minimal interface parsers to reduce the attack surface, but not the attack volume behind the attack surface. As PoC, formal langsec methods are adapted to reduce the attack volume of a pacemaker: A domain-specific language (DSL) translates requirements of a cardiac pacemaker patient and an information security researcher (ideally one and the same person) into an implantable minimum state space analog/mixed signal pacemaker application specific integrated circuit (ASIC). Such a minimum automaton methodology can be transfered to less life-critical IoT devices. ASICs for minimum automaton IoT designs are a use case for completely free CMOS IC fabrication processes, e.g., LibreSilicon. Non-essential state space that isn't implemented can't be hacked.
Why does this actually matter to end users?
Do you completely understand how your computer, laptop or smartphone works? Do you know what happens behind the browser, the text editor, the operating system? Probably not, and that is not a surprise nor is it something to be ashamed of. The development of consumer electronics is like a web that becomes increasingly intricate, where new technologies added continuously without anyone checking how the wires are connected or if there is a risk for short-circuiting. All sorts of vulnerabilities and back doors have crept in software and hardware over the years that even the developers themselves are sometimes unaware of.
You want technology you can trust. This becomes a matter of life and death when that technology helps keep you alive. To ask you one more question, do you know how an implanted medical device like a pacemaker works? And who can access and control it? Devices like pacemakers but also insulin pumps today are often connected devices, which essentially makes your body a part of the internet. And given the poor security of most so-called 'smart' devices, this puts patients using medical implants in a lot of danger.
This project aims to give people back control over their connected medical implants, starting with a secure and transparent pacemaker. Instead of creating a device with too much capabilities and a large attack surface, we can make single-purpose machines that only do what they need to do, using so-called langsec or language security design principles. Simply put, you do not have to shut a backdoor if there is no backdoor to begin with. Medical implants designed this way have a minimal attack surface and as such are more secure by design. Extending this approach to other connected devices can potentially solve the rampant security and privacy problem of 'smart' devices we are currently facing.
This project was funded through the NGI0 PET Fund, a fund established by NLnet with financial support from the European Commission's Next Generation Internet programme, under the aegis of DG Communications Networks, Content and Technology under grant agreement No 825310.
