Applying Unique Program Execution Checking in the development flow of industrial IoT devices to prevent vulnerabilities for side-channel attacks

Abstract

Nylige funn av sårbarheter i digitale design og datasystemer har understreket den økende betydningen av å klare å identifisere utnyttbare sidekanaler for å kunne produsere sikre systemer. I de verste tilfellene kan noen sårbarheter bli utnyttet for å få tak i passord og annen konfidensiell data. Metoden Unique Program Execution Checking (UPEC) er en teknikk innen formell verifikasjon som har blitt utviklet for å hjelpe til med å finne slike systemsårbarheter tidlig i utviklingsfasen. Tidligere har denne blitt testet ut på flere design, og den har greid å identifisere mulige sårbarheter ved disse systemene. Denne masteroppgaven har som mål å bruke UPEC metoden for å lete etter sårbarheter i den nyeste versjonen av PULPissimo plattformen samt designet nRF54L15 fra Nordic Semiconductor. Hensikten er å vurdere skalerbarheten av teknikken, ved å ta fatt i mål som tidsbruk per bevis som kjøres, samt minnebruk per bevis. Det blir også gjort ytterlige vurderinger, som å se på hvor mye forhåndskunnskap som er nødvendig, samt hvor arbeidskrevende det er å enten bevise, eller motbevise, tilstedeværelsen av sårbarheter. Selv om implementasjonen av metoden på nRF54L15 ikke ble oppnådd på grunn av problemer med oppsettet av systemet i det benyttede verktøyet OneSpin 360, ble det kjørt flere tester på PULPissimo plattformen. Dette førte til resultater angående metodens potensielle skalerbarhet, samt oppdagelsen av en sårbarhet. UPEC metoden er ganske avansert. Likevel viser resultatene som har blitt oppnådd og diskutert i dette eksperimentet at det kan være en god fremtidig teknikk for å finne systemsårbarheter. Med litt mer jobb, spesielt i forhold til opplæringsmaterialet som bidrar til å gjøre metoden mer forståelig og tilgjengelig, vil metoden kunne brukes på industrielle systemer.

Recently discovered vulnerabilities in digital designs and computing systems have highlighted the increasing importance of identifying exploitable side channels to ensure secure devices. In the worst scenarios, some vulnerabilities can be maliciously exploited to get hold of passwords and other confidential data. The Unique Program Execution Checking (UPEC) method is a formal verification technique developed to aid in the discovery of such system vulnerabilities during the early development phase. Previously, this has been tested out on several designs and it has been able to detect potential issues within these. This master's thesis aims to use the UPEC method to search for vulnerabilities in the newest version of the PULPissimo platform, along with the nRF54L15 design from Nordic Semiconductor. The goal to be accomplished is to assess the scalability of the technique, using the measurements of time-per-proof and memory usage per proof. Additional evaluations will also be conducted, such as how much knowledge is needed beforehand, along with how much manual effort is required to either prove, or disprove, the presence of vulnerabilities in the system. Although the application onto the nRF54L15 was not accomplished due to issues with the setup in the OneSpin 360 tool, several tests were run on the PULPissimo platform. This led to results regarding the UPEC method's potential scalability, and the discovery of a vulnerability within the system. The methodology is quite advanced, however, the results accomplished and discussed in this experiment show that this methodology might be a good technique in the future to locate system vulnerabilities. With a bit more work, especially on tutorials to make it more available and understandable, the method could be used on industrial systems.