Modellalapú statikus kódanalízis biztonságkritikus rendszerek fejlesztéséhez
A szoftverek esetén fontos a program helyes működése, ez különösen igaz biztonságkritikus szoftvereknél, amelyek hibái nemcsak jelentős anyagi kárt, de akár emberi életeket is követelhetnek. Éppen ezért ezeknek meg kell felelniük bizonyos szabványoknak, amelyek betartásával a helytelen működés könnyebben elkerülhető.
A biztonságkritikus és különösen a beágyazott rendszerek fejlesztése során a C nyelv az egyik legelterjedtebb, legszélesebb körben használt, hiszen ez egy jól bevált, kellően hardverközeli nyelv, amihez sok fordító és fejlesztőeszköz áll rendelkezésre. Nagy hátránya viszont, hogy túlságosan megengedő, így könnyen lehet benne csak futásidőben kiderülő hibát ejteni.
Az általános felhasználhatóság érdekében a C nyelvhez kapcsolódó szabványok (például MISRA C, CERT C) viszonylag nagy szabadságot biztosítanak a fejlesztőknek. Ebből a szabadságból eredően pedig a lehetséges hibák száma – habár kevesebb – még mindig jelentős.
A programok hibái gyakran csak a tesztelés során a szoftver futtatásával derülnek ki, így rengeteg időbe és pénzbe kerül ezek megtalálása és javítása. Egy statikus kódanalizátor szoftver ezzel szemben már fordításidőben jelzi a fejlesztőnek a problémákat, így azok akár a fejlesztés közben, azonnal javíthatók.
Szigorúbb nyelveknél (például típusellenőrzés szempontjából az Ada vagy a Haskell) már a fordítóprogram jelzi a felhasználónak a kisebb hibákat is. Ezek kiszűrésére C esetén nem elegendő egy fordító, hiszen a nyelv definíciója szerint ezek nem számítanak hibának, akkor se, ha hibás működést eredményeznek.
Dolgozatomban a C nyelven leírható kifejezések halmazát szűkítem le a nyelv kifejezőképességét nem korlátozva, viszont elősegítve a lehetséges hibák elkerülését. A C nyelvhez a létező szabványokhoz képest szigorúbb típusellenőrzést írok elő, továbbá lehetőséget nyújtok egy adott típus értékkészletének szűkítésére, valamint a típussal végezhető műveletek korlátozására, amely segítségével akár a fizikai dimenziók helyes kezelése is elérhető.
A C kód egyszerű kezelése érdekében azt a szoftver először az EMF (Eclipse Modeling Framework) segítségével megalkotott modellbe képezi le. Ehhez a modellhez gráfmintaillesztésen alapuló Viatra lekérdezéseket és validációs kényszereket fogalmaztam meg. Amennyiben a felhasználó által írt kód megszegi a szűkített C nyelv szabályait, a kódanalizátor szoftver az Eclipse integrált fejlesztőkörnyezetbe épülő, CDT-n (C / C++ Development Tooling) alapuló, saját fejlesztésű plugin segítségével jelez vissza.
szerző
-
Knoll Judit
Mérnök informatikus szak, mesterképzés
mesterképzés (MA/MSc)
konzulens
-
Dr. Suba Gergely
Osztályvezető, Prolan Irányítástechnikai Zrt. (külső)
