Hirdetésektől a pénzügyekig és az egészségügyig, személyes adatainkat egyre több alkalmazásban használják fel. E jelenség miatt a szenzitív információ megvédése a számítási architektúrák egyik legfontosabb elemévé vált.

Az ilyen jellegű alkalmazásoknak meg kell bízniuk a rendszerben, amin futnak, a rendszerszoftverek viszont annyira komplexek, hogy gyakran sebezhetők. A sebezhetőség kockáztatja az adatok titkosságát és integritását.

A Columbia Egyetem kutatói az elmúlt két évben a félvezető IP és szoftvertervező Arm-mal közösen dolgoztak ki verifikáló technológiát (Arm CCA) az Armv9-A architektúrához.

Az Arm CCA a hardver biztonsági garanciáit kezelő firmware-en alapul. Sok korábbi rendszer szintén firmware-alapú, viszont egyik sem garantálja, hogy azon nincsenek rések.

A formális verifikáció viszonylag új módszer, amely tényleg garantálja a hardver/szoftver „korrektségét.” Tesztelés helyett sokkal pontosabb matematikai módszerekkel ellenőrzi azt.

Egyszerű programok megbízhatósága többféle módszerrel verifikálható, de ezek a módszerek nem alkalmasak olyan komplex elemek vizsgálatára, mint az Arm CCA firmware. A kutatóknak ezért kellett új technikát kitalálniuk.

Az Arm CCA esetében fejlesztői alapelv, hogy nem megbízható szoftvernek is meg kell tartania a hardver-erőforrások kezelése feletti kontrollt, azaz a legfőbb kihívás a rendszer megbízhatóságának bizonyítása – annak ellenére is, hogy a nem megbízható szoftver tetszés szerint elvehet hardveres erőforrásokat. Korábbi módszerekkel ezt nem lehetett megvalósítani – klasszikus tesztekkel nehéz megtalálni a réseket –, az új technikával viszont igen.

Ezt sikeresen be is bizonyították, a verifikált firmware támogatja az architektúrát.

Arm CPU-kat világszerte többmilliárd eszközön használnak. Ha az Arm CCA is elterjed, és (főként a számítási felhőben) védi a felhasználó személyes adatait, az új verifikációs technika jelentős előrelépés lesz az adatvédelemben és a biztonságban.