Най-добрите практики за защита на превозни средства от хакери вече включват усъвършенствани техники за проверка.

Джон Холман, Дейвид Ландол, Siemens EDA
Не е тайна, че голяма част от управлението на съвременните превозни средства се осъществява чрез ИС и всеки достъп до тях може да даде на външен човек неканен контрол върху автомобила. Предизвикателство е да се идентифицират заплахите за сигурността, свързани с модерния автомобил, и да се гарантира, че превозното средство и пътниците са защитени. Поради многобройните възможности, вградени в електрониката на превозното средство, броят на заплахите за сигурността е доста висок, особено когато в анализа са включени уязвимости на ниско ниво на внедряване на IC.

Може да е полезно за инженерите, работещи в тази област, да заявят крайните цели или последствията от експлойт на сигурността с прости думи. Най-често срещаните резултати от пробив в сигурността на превозно средство включват (1) риск за личната безопасност, (2) финансова загуба, (3) разкриване на лична информация и (4) оперативна повреда на функция в самото превозно средство. Разработчиците, които просто се справят с всички известни заплахи, може да нямат достатъчно налични ресурси, за да постигнат обикновено агресивните цели за пускане на пазара. Следователно използването на последствията от пробив в сигурността ще помогне да се приоритизират и смекчат тези заплахи, които са най-подходящи.

Обикновено прилаганите практики за системно инженерство, изискванията за сигурност и последващите смекчаващи мерки се спускат надолу към ниво IC. Тези смекчаващи мерки могат да приемат много различни форми. Важна референция за автомобилното инженерство за сигурност е стандартът „ISO/SAE DIS 21434 Пътни превозни средства – Инженеринг за киберсигурност.” Внедряването на защитени дизайнерски структури като доверени платформени модули (TPM), блокове за криптиране на данни или излишни пътища за обработка на данни са само няколко примера за проектирана сигурност.

Има много налични най-добри практики, които да помогнат за смекчаване на заплахите за превозно средство, но тук се фокусираме върху проверката за смекчаване на сигурността и необходимостта от по-усъвършенствани методи за проверка.

В продължение на десетилетия основните методи за проверка на системи и цифрови IC функции са базирани на симулация техники. Симулацията разчита на тестова стенда (основно контейнер, където дизайнът се поставя и задвижва с различен входен стимул) и входен стимул. Стимулът взаимодейства с цифров модел на дизайна, опитвайки се да подражава на поведението на реалната среда, в която IC ще работи. По-простите методи за изпитване, известни като насочени тестове, просто разчитат на хората да дефинират ръчно конкретна последователност от тестови вектори, за да стимулират дизайна с поток от входни данни, като междувременно проверяват дали дизайнът реагира правилно на тази конкретна последователност.

Очевидното ограничение на този метод е, че той тества само специфични поведения в специфичния ред и време, както е определено от създадените от човека тестови вектори. По-сложни техники, базирани на симулация, се опитват да заобиколят това ограничение чрез включване на ограничен произволен стимул, обикновено написан на по-усъвършенстван тестов език като SystemVerilog или System C. Ограничен произволен стимул позволява на тестовия стенд да променя точното време, последователност и съдържание на различни видове транзакции и входни сигнали. Правилното поведение на дизайна обикновено се проверява спрямо референтен модел, който предвижда как дизайнът трябва да реагира на ограничения случаен стимул.

Тази процедура повдига въпроса „Как да разбера какво е проверил този тестов стенд?“. Отговорът обикновено се търси чрез различни видове анализ на покритието, които измерват колко пъти различни транзакции са били изпробвани с какви типове съдържание. Различни видове „кръстосано покритие“ също могат да бъдат използвани (измерване, например, колко пъти се е случила определена транзакция, докато прекъсването е получено едновременно, или дори просто превключване на покритието на регистър или сигнал). Този тип процедура е широко използвана за модерна проверка на IC.

Но тази методология все още е недостатъчна. Той проверява само поведението на IC, което тестовата стенда е написана, за да стимулира. И променя стимула само в рамките на диапазона, за който е програмиран да проверява (и обикновено е доста по-малко от изчерпателна проверка на функцията). Освен това, той измерва само онези аспекти на покритието, които са зададени ръчно. Много просто, базираните на симулация техники за проверка могат да стимулират само ограничено количество поведение. Следователно, дадена IC може да бъде добре проверена спрямо изискванията си, но може да се държи неправилно, когато бъде стимулирана извън оперативните очаквания, включени в стимула на тестовия стенд.

Това е проблем, защото много съвременни пробиви в сигурността се възползват от неочаквания отговор на IC на неочакван стимул. Целта на нападателя е да идентифицира поведението на стимула, което може да се използва, за да накара дизайна да направи нещо неочаквано. В много случаи грешка или слабост в дизайна на IC, която не е била уловена по време на процеса на проверка, предлага отлична възможност за експлоатация. В най-простия случай нападателят може да активира грешка или нежелана функция в дизайна, която изстрелва хардуера в уязвимо състояние. Примери за такива уязвимости включват препълване на FIFO или блокиране на държавна машина.

Нападателят може също така да активира схема на проектиране, която не е предназначена да бъде достъпна за обща употреба, като активиране на логика на ранен прототип или логика в тестов режим, която позволява достъп до иначе защитени зони на устройство. В други случаи могат да бъдат създадени различни слабости, като просто се остави на място кодът, необходим за разработката, но след това се изостави без премахване – например оставяне в допълнителни неизползвани състояния за машина със състояния, която по-късно се ревизира, за да използва по-малко състояния. И накрая, проектен инженер с престъпни намерения може да вмъкне функции за бъдещи хакове, като добавяне на „задна врата“ с адрес и ключ за отключване, които само лицето знае.

Единственият начин да се предпазите от тези уязвимости е да проверите всяко възможно поведение през цялото време. За съжаление, в съвременните интегрални схеми тази обширна проверка е по своята същност неразрешима чрез техники, базирани на симулация. Би било аналогично на боядисването на всички сгради в Ню Йорк с една-единствена четка за зъби – теоретично възможно, но невъзможно в смисъл на реалния свят. Следователно допълнителни методи за допълване на симулацията са много необходими за справяне със заплахите и уязвимостта.

Ползите от формалните методи

За щастие има подход за проверка, който допълва симулацията и е много подходящ за откриване на непредвидими проблеми. Официалната проверка използва изчерпателни математически алгоритми за проверка на функционалността на дизайна спрямо неговите изисквания и съществува от десетилетия. Тъй като процесът е изчерпателен, отговорът на въпроса „Този ​​дизайн винаги ли реагира правилно?“ е гарантирано пълно – за всички възможни стимули през цялото време. Тоест, ако дизайнът на дигитален хардуер може да покаже някакво нежелано поведение, формалните методи ще го посочат.

От друга страна, ако такова нежелано поведение не съществува, тогава формалните методи ще го кажат. Когато се използва по време на фазата на проектиране на проект, хардуерен инженер може да започне да проверява дизайна, преди да е наличен тестов стенд, базиран на симулация. Официалната проверка автоматично ще създаде изчерпателен стимул. Инженерът просто трябва да зададе някои често срещани въпроси относно дизайна, като например „Моят FIFO винаги ли се държи правилно, без изобщо да препълва?“ или „Тази държавна машина винаги ли ще преминава правилно, без НИКОГА да бъде блокирана?“ или „Моят дизайн ВИНАГИ елегантно ще открива и ще отговаря на ВСИЧКИ възможни законни И незаконни инструкции?“ и т.н. Тези типове поведение лесно се проверяват чрез формална проверка.

Представете си ситуация, при която елементът на паметта на автомобилната система е защитен от ECC (Код за коригиране на грешки). Целта на ECC е да открие и евентуално да коригира битове на паметта, повредени от електромагнитни смущения. Но какво ще стане, ако грешка в паметта остане неоткрита? Това условие може да доведе до изпълнение на незаконна инструкция или погрешно или нестабилно поведение от автономна система. Този тип логика за възстановяване на грешка е трудна за цялостна проверка чрез традиционните неформални техники за проверка поради големия брой възможни повреди, комбинирани с възможното време на тези повреди. Симулацията би изисквала неразрешимо време за проверка дори на малка част от възможните ситуации, така че е лесно проблемите в тази логика да останат незабелязани чрез процеса на проектиране и проверка на хардуера. Официалната проверка обаче може изчерпателно да провери всички възможни функционални поведения през цялото време, за да гарантира, че получената логика за откриване на грешки и възстановяване винаги ще реагира правилно.

Представете си друга ситуация, свързана със спирачната система на автомобила. Да предположим, че IC агрегати за управление на спирачките от автономна бордова система за самостоятелно управление, от инициирано от водача ръчно управление и от механизъм за безопасност при повреда на системата в случай на проблем. Ако всички тези системи от по-високо ниво започнат да се борят за контрол върху спирачките, наложително е IC да управлява спирачната система по предвидим начин. Възможните взаимодействия на тези системи обаче са сложни – добавете към тях евентуално престъпно хакване на системата от лош актьор или всякакви други възможни скрити или неуточнени функции и задачата за проверка просто става неразрешима чрез традиционните механизми. Симулационните тестови вектори не биха могли да реализират висока степен на покритие за податлив период от време.

Формалната проверка обаче може изчерпателно да провери всички възможни контролни взаимодействия чрез свойства и функционални описания, като гарантира, че системата винаги ще се държи предвидимо и надеждно. По време на процеса на проверка инженерите по проверка могат да използват формални методи, за да гарантират, че изискванията за дизайн са НАПЪЛНО изпълнени, че функциите за сигурност не могат да бъдат достъпни през незащитени канали, че дизайнът винаги ще се справи с всяко неочаквано поведение при въвеждане и че няма допълнителни функции или задни врати, които проверката, базирана на вероятностна симулация, може да пропусне.

В допълнение, формалната проверка може да се използва и за проверка на дизайна срещу други видове натрапчиви атаки, като например ЕМП импулси, които се опитват да принудят дизайна в неизвестно състояние. Например, представете си, че една спирачна система съдържа блок от производствено-тестова логика, която позволява пълен вътрешен достъп, но трябва да бъде изключена и недостъпна по време на нормална проектна дейност. Може ли НЯКОГА тази логика да бъде достъпна по неочакван или неподходящ начин?

пример за хакванеХакер може лесно да закупи и използва локализиран източник на нискоенергийни рентгенови лъчи, като малък ръчен стоматологичен рентгенов апарат (достъпен само за $500). Насочено директно към IC, неговото излъчване може да бъде достатъчно, за да накара изолиран регистър в IC да обърне стойностите. Сега помислете за сценарий на атака, при който IC, обработваща тестов достъп, може да бъде инициализирана в режим „без достъп“ при стартиране на системата. Въпреки това, произволно обръщане на един бит в регистъра на държавната машина може лесно да постави чипа в активен режим (напр. обръщане на двубитов регистър от 00 на 10), активирайки тестовата логика – като по този начин позволява на нечестив актьор достъп до други ограничени функции. Хардуерните проекти могат и трябва да бъдат изградени, за да издържат на атаки като тази. Официалните методи могат да упражняват всички възможни смущения в регистъра чрез техники за инжектиране на грешки, за да се гарантира, че дизайнът никога няма да се окаже в уязвимо състояние.

Разбира се, предизвиканите от радиация преобръщания на битове като това не се дължат непременно на нападател. Те могат също да бъдат повреди, причинени от естествени източници на радиация, други ситуации на статично разреждане или дори електромиграция в самия чип. (За по-задълбочено разбиране на тези рискове вижте J. Grosse, S. Marchese, „Fault Injection Made Easy,“ DVCon India 2017.) Откриването и в крайна сметка коригирането на тези неизправности са изключително важни както за безопасността, така и за сигурността на автомобила .

С помощта на нововъзникващите стандарти, като ISO/SAE 21434, всички можем да разберем по-добре предизвикателствата на заплахите за киберсигурността. Тези стандарти и практики също така помагат на автомобилните разработчици да създават по-безопасни и по-сигурни автомобили чрез използване на сигурни дизайнерски практики и по-добри методи за проверка на сигурността. Усъвършенстваните техники за проверка помагат за разширяване на традиционните практики и предоставят ценните инструменти, необходими за справяне с нарастващата сложност, прилагана в днешните интегрални схеми. Дойде времето да превърнем сигурността в основен приоритет и да възприемем официалните методи и други техники за проверка за намаляване на сигурността като част от процеса на разработване на превозни средства.

Securing automotive ICs with formal methods

Previous articleShackle raises $5.5M to digitize hotel guest experience
Next articleInstagram is reportedly testing a BeReal-like Candid Challenges feature