Egy korábbi cikkben már írtam arról, hogy egy rendszer fogalmi modelljének helyességét hogyan tudjuk vizsgálni, a rendszer dinamikus működésének “helyességéről” viszont akkor nem beszéltünk. Ebben a cikkben arra próbálunk választ keresni, hogy van-e lehetőségünk arra, hogy a rendszerünk működését modell szinten vizsgáljuk, ellenőrizzük, és ha logikai hibát találunk, azt jelezzük.
Kétfaktoros autentikáció modellje
Az elmúlt időben azonban előjött egy feladat – mobil alapú kétfaktoros autentikáció -, ahol arra volt szükség, hogy megnézzük, hogy a rendszer, illetve a rendszerben párhuzamosan futó folyamataink hogyan működnek együtt; létezik-e olyan állapotátmenet a rendszer futása során, amikor hibás állapotba kerülünk.
A kétfaktoros autentikáció során a felhasználó két faktorral tud csak belépni a rendszerbe, az első faktora a felhasználó azonosító és jelszó kombinációja, a második pedig egy sms-ben megkapott kód, vagy pedig a mobil alkalmazásban történő engedélyezés.
Maga a folyamat a következőképp néz ki: a felhasználó weben indít egy belépést a felhasználó-azonosítója és jelszava megadásával. Ezután a mobil telefonjára kap egy értesítést, melyre kattintva be tud lépni a mobil alkalmazásba, és engedélyezni tudja az adott belépési próbálkozást. Ezen engedély megadásának hatására megtörténik a belépés a weboldalon. Előfordulhat azonban, hogy a mobil alkalmazás nem működik, vagy éppen nem elérhető, ezért ilyenkor is lehetőséget kell biztosítani a felhasználónak arra, hogy be tudjon lépni. Ezt a legtöbbször úgy oldják meg, hogy a felhasználó a web felületen egy linkre kattintva egy SMS kódot kap a korábban regisztrált telefonszámára. Ezt a kódot amennyiben helyesen visszaírja a weboldal felületére, akkor be tud jelentkezni.
A folyamat modellezésére kiváló eszközünk az állapotgép diagram, ahol az egyes képernyőket állapotonként, a képernyők közötti átmenetet eseményekként fogjuk modellezni.
A rendszer két párhuzamosan futó folyamatból áll: a felső a web alkalmazás állapota, az alsó a mobil alkalmazás folyamata.
A web alkalmazás a login képernyő állapot után a távoli belépést engedélyezéséhez tartozó képernyő állapotba kerül, ahol is létrejön a rendszerben egy remote authentication request, mely a belépési kérelmet reprezentálja. Ezt vagy elfogadja a felhasználó, és akkor a belépett képernyőt reprezentáló állapotba visszük a rendszert, vagy pedig sms-re vált, ekkor a korábban létrehozott engedélyezési kérelmet törölni fogjuk. Az sms megadása esemény hatására a rendszer ugyancsak a belépett képernyő állapotba kerül.
Látható, hogy több hibaágak nem modelleztünk: mi történik, ha elutasításra kerül a kérelem, mi történik, ha a folyamat egyszerűen meghal (mert például bezárja a felhasználó a böngészőt), stb. Ez egy tudatos döntés eredménye, megpróbáltuk a rendszert a lehető legegyszerűbben modellezni, a valóságban ennél nyilván majd komplexebb modell-t fogunk alkotni.
A mobil alkalmazás a belépés (Mobile login screen) után lekérdezi a belépési kérelmet (QueryRemoteAuth állapot), és ha nem talál, akkor a fő képernyőre (Mobile logged in screen) visz. Ha talál, akkor feldob egy döntési képernyőt (Remote auth decision screen) ahol a felhasználó a szerint, hogy elfogadja (grant) vagy elutasítja (reject), akkor a belépést engedélyező (Remote auth granted screen) vagy elutasító (Remote auth rejected screen) képernyőre kerül. Ha ezeket a képernyőket bezárja, akkor a belépett (mobile loggen in screen)-re kerül.
Itt sem érdemes abba belebonyolódni, hogy miért is mutatunk bármilyen képernyőt a döntésről, miért nem csináljuk azt, hogy a döntés hatására rögtön a belépett képernyőre megyünk, igazából nincs jelentősége.
Nézzük meg tehát, hogy van-e olyan ág, amelyiknél hiba léphet fel. A lenti ábrán egy ilyen lefutást találunk.
A felhasználó belépett weben, létrejött az engedélykérés, majd belépett mobilon, és megjelent az engedélyező képernyő. Ezután weben visszavált SMS-re, viszont a mobil erről nem fog tudni, tehát ha akár engedélyezést (grant), akár elutasítást (reject) választ, egy olyan engedély kérelemmel kapcsolatban fog döntést hozni, melyről már korábban döntést született (cancel-álva lett). Ez egy logikai hiba, amit kézzel, próbálkozással idéztünk elő.
A lényeg a logikai hiba: teljesen mindegy, hogy milyen programozási nyelvet, milyen paradigmát, milyen fejlesztő eszközt, milyen módszertant használunk, a logikai hiba ettől még ott lesz, ezeket fel kell fedni, és megpróbálni javítani vagy körbetákolni.
A legjobb az lenne, ha nem kézzel kellene végignyomogatni illetve végiggondolni az összes lehetőséget (amely 3-4 párhuzamos folyamat, 4-5 állapotváltozó esetén nagyjából esélytelen), hanem a feladatot egy szoftverre bíznánk, mey végigmenne a teljes állapottéren kipróbálva az összes lehetőséget, vizsgálva, hogy az előre lefektetett invariánsok (szabályok, melyeknek mindig teljesülnie kell) sértése megtörténik-e, és ha igen, akkor mi volt az az állapot átmenet sorozat, mellyel a szabálysértést reprodukálni lehet.
TLA+ formális specifikációs eszköz
A fenti feladat megoldására egy eszköz a TLA+.
A TLA+ egy formális specifikációs nyelv, melyet Leslie Lamport talált ki. A nyelv önmagában matematika formulákkal dolgozik, szerencsére létezik hozzá egy PlusCal nevű előtét nyelv, mely sokkal közelebb áll a legtöbbek által ismert “hagyományos” programozási nyelvhez, ezért inkább ezt fogjuk használni.
A TLA+ rendelkezik egy Eclipse alapú fejlesztői környezettel – ezt ők toolbox-nak hívják -, a feladat megoldásához ezt fogjuk használni, mely letölthető a következő címről:
https://github.com/tlaplus/tlaplus/releases/tag/v1.7.1
A TLA+ és a PlusCal teljes megismerése messze túlmutat a cikk keretein, a feladat megoldásához ezek egy minimális részhalmazát fogjuk használni.
Modell és PlusCal megfeleltetés
A következő táblázat azt a megfeleltetést mutatja be, amely segítségével a feladatban található elemeket át tudjuk fordítani PlusCal nyelvi elemekre.
| Feladatbeli elem | TLA/PlusCal elem |
| Global state | global variable |
| Orthogonal region | process |
| Current state | process szintű variable |
| State | label a hozzá tartozó vizsgálattal |
| State transition | értékeadás a process szintű variable-nek |
| State action | label-hez tartozó kód |
| Assertion | assert |
Global state modellezése
Szükségünk lesz egy globális állapotra, melyet a folyamatainkon kívül definiálunk. Ezt a globális változót fogja mindkét folyamat olvasni illetve írni. A jelen feladathoz egy String típusú globális változó elegendő, komplexebb esetben használhatunk struktúrákat is.
variables remoteAuthState = "NULL";
A lehetséges adattípusokról bővebben a következő oldalon olvashatunk:
https://learntla.com/reference/types/
Orthogonal state modellezése
A párhuzamosan futó folyamatokat a state diagram-ban orthogonal region-nal modellezzük. A TLA rendelkezik egy process fogalommal, mely egy folyamatot jelképez.
process webProcess = 1
variables
webProcessState = “Start”,
run = TRUE;
begin P:
while run do
<<ide jön a kód>>
end while;
end process;
Minden process rendelkezik egy névvel (webProcess) és egy azonosítóval (1). Ebből a folyamatból egyetlen példány fog elindulni, de lehetőség van arra is, hogy több példányt indítsunk.
A folyamat rendelkezhet folyamat szintű változókkal, melyek az adott folyamat példányhoz tartoznak. Ezeket a változókat a folyamat deklarációján belül, a variables kulcsszó segítségével tudjuk megadni. A példában egy webProcessState nevű változót definiálunk, amely String típusú, és a Start értéket veszi fel induláskor; illetve egy run nevű változót, mely segítségével biztosítjuk azt, hogy a folyamatunk addig fusson, amíg egy terminális állapotba nem kerül.
A folyamatokról bővebben a következő oldalon olvashatunk:
https://learntla.com/concurrency/processes/
State modellezése
Az egyes állapotokat egy címkével (label-lel), és egy kapcsolódó guard feltétellel tudjuk modellezni:
StartWebProcess: if webState = “Start” then <<ide jön a kód>> else skip; end if;
Minden egyes állapothoz egy label-t hozunk létre. A label a TLA rendszerben egy lépést reprezentál, minden, az adott label-hez tartozó kód egy lépésben fog lefutni.
A label-ekkel kapcsolatos szabályokról a következő oldalon olvashatunk:
https://learntla.com/concurrency/labels/
Az adott lépésben megvizsgáljuk, hogy a folyamat állapota az-e, amely esetén kódot akarunk végrehajtani, ha pedig nem, akkor nem csinálunk semmit (skip).
State transition modellezése
Az állapot átmeneteket ebben az egyszerűsített modellben az adott folyamathoz tartozó, az adott folyamat aktuális állapotát jelképező folyamatszintű változó állításával oldjuk meg. Azon esetekben amikor több választási lehetőség van, az either/or párost használhatjuk.
RemoteAuthScreen:
if webState = “RemoteAuthScreen” then
either
webState := “WebLoggedInScreen”;
or
webState := “SmsScreen”;
end either;
else
skip;
end if;
State action modellezése
A folyamat egyes lépéseiben különböző műveleteket hajthatunk végre. Az State Diagram több csatlakozási pontot is definiál amelyhez akciókat tudunk kötni (entry, do, exit), mi ezt leegyszerűsítjük: az állapotba való belépésnél (entry) hajtunk végre utasítás sorozatot, a korábban definiált globális változót fogjuk állítani.
remoteAuthState := "Undecided";
Assertion modellezése
A feladat megoldása során azt szeretnénk vizsgálni, hogy a mobil eszközön történő engedély elfogadása vagy elutasítása pillanatában az adott engedéllyel kapcsolatban történt-e már döntés.
Általánosítva azt mondhatjuk, hogy a programunk futása során, egy adott pillanatban azt szeretnénk vizsgálni hogy a rendszer (vagy az adott folyamat) állapota megegyezik-e az általunk elvárttal. Ha nem, akkor azt várjuk el, hogy a futtató környezet hibát jelezzen.
Erre szolgál az assert kulcsszó.
assert remoteAuthState = "Undecided";
Modell-ellenőrzés
A fenti szabályokból már egyszerűen össze tudjuk állítani a specifikációnkat, mely egyébként elérhető a
https://github.com/sz332/tla_login_statemachine/blob/main/statemachine.tla
címen.
A TLA toolbox elindítása után hozzunk létre egy új Spec-et a File → Open Spec → Add New Spec alatt.
Egy új könyvtárban létre fog jönni egy új specifikáció, ahová egyszerűen másoljuk be a fenti példa kódot.
Amennyiben nem statemachine-nak neveztük el a könyvtárunkat, a rendszer hibát fog dobni, ezért írjuk át a MODULE statemachine részt az általunk adott modulnévre.
Ezután a PlusCal forrásból a CTRL + t kombinációval fordítsunk TLA+ kódot.
Ha elkészült a TLA+ kód, akkor hozzunk létre egy modell-t, amelyen a specifikációnkat futtatni fogjuk.
Ezt a TLC Model Checker → New Model… menüpontban tudjuk megtenni. Adjunk egy nevet a modellünknek, majd pedig állítsuk be.
Azt akarjuk vizsgálni, hogy a specifikációnk lefut, tehát a What to check pontban kattintsuk be a Termination beállítást.
Ezután a futtatás gomb megnyomásával indítsuk el a modell validációt. Láthatjuk, hogy a rendszerben hiba történt, nem tudott befejeződni.
Kattintsuk a TLC Errors fülön található Failure of assertion at … linkre, melynek hatására a szerkesztő arra a sorra ugrik, ahol a hiba történt.
Az elvárásainknak megfelelően ott futottunk hibára, ahol vártuk: amint egy engedélyt próbálunk adni, addigra a távoli belépésről már döntés született.
Az Error-Trace ablakban végig tudjuk követni, hogy milyen állapotátmenet során történt a hiba.
Az egyes állapotok átmeneteiből pontosan azt látjuk, amit vártunk: ha a webes belépés után a mobilon belépünk, akkor azt fogjuk látni, hogy van egy engedélykérés, a weben SMS-re váltunk, ezáltal töröljük az engedélykérést, majd pedig mobilon választunk (akár elfogadást akár elutasítást). Ebben a pillanatban azt fogjuk látni, hogy már döntés történt az adott engedélykérésről, és hibára fogunk futni.
Összefoglaló
A cikkben megvizsgáltuk, hogy a párhuzamosan futó folyamatokból álló rendszer dinamikus működését hogyan tudjuk state diagram segítségével ábrázolni, és ezt a diagramot hogyan tudjuk TLA+ szabályokba átalakítani. Az átalakítás után szabályokat fogalmaztunk meg, melyek teljesülését model-analízis segítségével ellenőriztük. Kiderült, hogy a rendszerben logikai hiba található, melyhez vezető állapot-átmeneteket a TLA+ rendszer – elvárásainknak megfelelően – megmutatta.
Fejlesztési irányok
A cikkben egy nagyon egyszerű, részleges, számunkra “elég jó” megoldást írtam le. Ha érdekesnek találtad, és szeretnéd tovább vinni, akkor van néhány ötletem illetve javaslatom, amivel az adott megoldást tovább lehetne fejleszteni, hogy még kényelmesebb, használhatóbb legyen.
- Nem csak részleges, hanem teljes UML statechart konverzió
- OCL kifejezések konverziója TLA+ assert-ekre
- Kézi transzformáció helyett model-transzformáció például Ecore/UML alapokon
- Magicdraw plugin fejlesztése, mely automatikusan végrehajtja a konverziót és mutatja a hibákat
