Нова обчислювальна архітектура захищає конфіденційні особисті дані
Оскільки наші особисті дані все частіше використовуються в багатьох програмах, від реклами до фінансів і охорони здоров’я, захист конфіденційної інформації став важливою функцією комп’ютерних архітектур. Програми, які обробляють такі дані, повинні довіряти системному програмному забезпеченню, на яке вони покладаються, наприклад операційним системам і гіпервізорам, але таке системне програмне забезпечення є складним і часто містить вразливості, які можуть загрожувати конфіденційності та цілісності даних.
Протягом останніх двох років дослідники з Columbia Engineering працювали з Arm, провідною компанією з розробки інтелектуальної власності та програмного забезпечення, щоб усунути ці вразливості. Зараз команда оприлюднила ключові технології перевірки для конфіденційної обчислювальної архітектури Arm (Arm CCA), нової функції архітектури Armv9-A.
Arm CCA покладається на вбудоване програмне забезпечення для керування апаратним забезпеченням, щоб забезпечити гарантії безпеки, тому дуже важливо, щоб мікропрограмне забезпечення було правильним і безпечним. Хоча багато попередніх систем покладаються на прошивку, жодна з них не може гарантувати, що прошивка не має помилок. Формальна перевірка є відносно новою методологією, яка зараз використовується для гарантії коректності програмного/апаратного забезпечення. Замість тестування формальна перевірка використовує математичні моделі, щоб довести, що програмне та апаратне забезпечення є абсолютно правильними, і, таким чином, забезпечує найвищий рівень гарантії правильності.
«Ми вперше довели, що вбудоване ПЗ є правильним і безпечним, що призвело до першої демонстрації конфіденційної обчислювальної архітектури, підкріпленої офіційно перевіреним мікропрограмним забезпеченням», — сказав провідний автор дослідження Сюпен Лі, доктор філософії.
Хоч існує багато підходів до перевірки правильності простих програм, вони не підходять для чогось такого складного, як прошивка CCA, тому дослідникам довелося розробити нові методи перевірки, щоб зробити перевірку прошивки Arm CCA можливою. Наприклад, мікропрограмне забезпечення CCA розроблено для масштабованості та продуктивності, тому воно забезпечує високопаралельну роботу та змішує C і асемблерний код. Одночасна робота стає можливою завдяки використанню методів тонкої синхронізації та коду з перегонами даних.
Принцип розробки Arm CCA полягає в тому, що ненадійне програмне забезпечення має зберігати контроль над керуванням апаратними ресурсами, тому ключовим завданням є доведення того, що система все ще безпечна, навіть якщо ненадійне програмне забезпечення може забрати апаратні ресурси, як заманеться. Попередні підходи не змогли перевірити програми з такими властивостями. Ця нова техніка перевірки є достатньо потужною, щоб перевірити одночасне мікропрограмне забезпечення як на C, так і на асемблері.
Команда дуже захоплена новими технологіями перевірки, які можна використовувати для підтвердження правильності реалізацій мікропрограми, що лежить в основі Arm CCA. Процесори Arm вже розгорнуті на мільярдах пристроїв по всьому світу. Оскільки Arm CCA стає все більш поширеним для захисту особистих даних користувачів, особливо в хмарних службах і за їх межами, методи перевірки, продемонстровані в цій статті, забезпечать значне покращення захисту та безпеки даних.
Однією з проблем формальних методологій, що застосовуються до програмного забезпечення, є необхідність адаптувати докази під час оновлення програмного забезпечення. Дослідники працюють над новими технологіями, які допоможуть їм поступово та швидко перевіряти оновлення мікропрограми Arm CCA та гарантувати, що найновіша доступна мікропрограма завжди перевіряється.
За матеріалами: Techxplore