Formaali verifiointi turvallisuuskriittiselle puolustusohjelmistolle

Ohjelmistovirhe kaupallisessa sovelluksessa maksaa yritykselle rahaa ja haittaa käyttäjiä. Ohjelmistovirhe aseiden tulenhallintalaitteistossa, ilma-aluksen lennonhallintayksikössä tai ydinaseiden komentolaitteistossa voi aiheuttaa peruuttamattomia fyysisiä vahinkoja. Seurausten epäsymmetria on niin äärimmäinen, että tavanomainen lähestymistapa ohjelmiston laatuun — kirjoita koodi, aja testit, korjaa testien löytämät virheet — on riittämätön. Testaus voi osoittaa virheiden olemassaolon, mutta ei niiden poissaoloa. Kaikkein kriittisimmälle puolustusohjelmistolle insinööriyhteisö on vastannut tähän rajoitukseen formaalilla verifioinnilla: matemaattisesti tiukoilla tekniikoilla, jotka todistavat ohjelmiston käyttäytymisen olevan oikeaa rakenteellisesti, ei pelkästään otannalla.

Tämä artikkeli on käytännöllinen tekninen viite formaalien menetelmien soveltamiseksi turvallisuuskriittiseen puolustusohjelmistoon. Se kattaa sääntelykehyksen, joka pakottaa formaalin verifioinnin korkeimmilla kriittisyystasoilla, tärkeimmät työkalut ja tekniikat (TLA+, SPARK Ada, CBMC, Frama-C), protokollan verifioinnin erityishaasteen mallintarkistuksen avulla sekä formaalien artefaktien integroinnin DO-178C-vaatimustenmukaisuusnäyttöön. Artikkeli päättyy kustannus-hyötyanalyysiin, joka antaa ohjelmapäälliköille viitekehyksen päättää, milloin formaali verifiointi on ylimääräisen työn arvoista — ja milloin se on yksinkertaisesti pakollista.

Milloin formaali verifiointi vaaditaan puolustusohjelmistossa

Velvoite formaaliin verifiointiin puolustusohjelmistossa syntyy kahden sääntelykehyksen risteyskohdassa: järjestelmäturvallisuusstandardin MIL-STD-882E, joka luokittelee vaarat seurausten vakavuuden ja todennäköisyyden mukaan, sekä ohjelmistokehitysstandardien, jotka muuntavat nämä luokitukset ohjelmistotekniikan velvoitteiksi.

MIL-STD-882E määrittää kullekin ohjelmistofunktiolle ohjelmistokriittisyysindeksin (SCI) seurausten vakavuuden (Katastrofaalinen — hengen tai järjestelmän menetys; Kriittinen — vakava vamma tai merkittävä järjestelmävaurio; Marginaalinen — lievä vamma tai järjestelmävaurio; Merkityksetön) ja todennäköisyyden tulona. Katastrofaaliseksi arvioidut toiminnot saavat SCI-kategoria I:n todennäköisyydestä riippumatta, koska mikään katastrofaalisen lopputuloksen todennäköisyys insinöörillisen huolimattomuuden kautta ei ole hyväksyttävää. Kategoria I -toiminnoille on tehtävä kaikkein tiukin käytettävissä oleva ohjelmistoturvallisuusanalyysi — mikä nykyään tarkoittaa formaalia analyysia.

Ilmailu- ja ilmailuun liittyville asejärjestelmille (ohjukset, ohjatut ammukset, joissa on lennonhallintaohjelmisto) sertifiointistandardi on DO-178C. DO-178C määrittelee viisi suunnittelun varmistustasoa (DAL A–E), ja taso A on varattu ohjelmistolle, jonka vika voisi aiheuttaa katastrofaalisen vikatilanteen tai myötävaikuttaa siihen. Taso A asettaa 66 ohjelmistokehitys- ja verifiointitavoitetta, mukaan lukien:

• 100 % muokattu ehto/päätöskattavuus (MC/DC) — jokainen ehdon itsenäinen vaikutus päätökseen on osoitettava
• Verifiointitoimintojen riippumattomuus kehitystoiminnoista
• Työkalujen kvalifiointi DO-330:n mukaisesti kaikille työkaluille, joita käytetään vaadittujen verifiointitoimintojen poistamiseen
• Formaali analyysi (DO-333-lisäyksen kautta) vaihtoehtoisena vaatimustenmukaisuuden osoittamiskeinona rakenteellisen kattavuuden tavoitteille

DO-178C:n DO-333-lisäys käsittelee nimenomaisesti formaaleja menetelmiä keinona täyttää verifiointitavoitteet. Kun ohjelma soveltaa formaalia verifiointia DO-333:n mukaisesti, sen on laadittava formaalien menetelmien suunnitelma, jossa kuvataan valittu formalismi, verifioitavat ominaisuudet, käytetyt työkalut ja miten formaaliverifiointinäyttö vastaa DO-178C:n taulukoiden A-3–A-7 tavoitteita.

Maakuntaisten ja merivoimien asejärjestelmille, joihin DO-178C ei suoraan sovellu, vastaava polku kulkee MIL-STD-882E Kategoria I -vaatimuksista ohjelmakohtaisiin ohjelmistokehityssuunnitelmiin, joissa viitataan yhä enemmän formaalin analyysin tekniikoihin seurausten vakavuuteen suhteutettuna tiukkuuden osoituksena. Missiokriittisen ohjelmistoarkkitehtuurin päätökset, jotka määrittävät mitkä komponentit saavuttavat Kategoria I:n tai DAL A:n, on tehtävä varhaisessa järjestelmäsuunnittelussa — ne ovat tärkein verifiointikustannuksen ajuri.

Määrittely ennen koodia: formaali malli

TLA+ (Temporal Logic of Actions, Leslie Lamportin kehittämä) on laajimmin käytetty formaali määrittelykieli hajautetuille järjestelmille ja tilakoneen protokollille puolustusohjelmistossa. TLA+-määrittely kuvaa järjestelmän tilamuuttujajoukkona ja toimintajoukkona — siirtyminä, jotka muuttavat tilaa — matemaattisessa merkinnässä, joka on yksiselitteinen ja koneellisesti tarkastettavissa.

Keskeinen oivallus on, että TLA+-määrittelyt kirjoitetaan ennen toteutuksen aloittamista. Tämä ei ole pelkästään hyvä käytäntö; se on mekanismi, jolla formaalit menetelmät löytävät virheet, jotka testaus ei havaitse. Testit harjoittavat käyttäytymistä, jonka testaaja ennakoi. Formaali malli, jonka TLC-mallintarkistaja tarkastaa kattavasti, harjoittaa kaikkia määrittelyn sallimia käyttäytymisiä — mukaan lukien käyttäytymistä, jota määrittelijä ei tietoisesti harkinnut.

Harkitaan yksinkertaistettua esimerkkiä aseiden laukaisun valtuutusprotokollasta. Protokolla vaatii, että laukaisukomento suoritetaan vain, kun molemmat miehistön jäsenet ovat itsenäisesti tunnistautuneet ja molemmat ovat nimenomaisesti valtuuttaneet laukaisun määritetyn aikaikkuna sisällä. Luonnollisella kielellä ilmaistu vaatimus voi esittää tämän selkeästi. Mutta formaali määrittely on tehtävä jokaisesta tilasiirtymästä eksplisiittisenä:

VARIABLES pilot_auth, copilot_auth, pilot_authorized,
          copilot_authorized, release_executed, time_window_open

TypeInvariant ==
    /\ pilot_auth       \in BOOLEAN
    /\ copilot_auth     \in BOOLEAN
    /\ pilot_authorized \in BOOLEAN
    /\ copilot_authorized \in BOOLEAN
    /\ release_executed \in BOOLEAN
    /\ time_window_open \in BOOLEAN

SafetyInvariant ==
    release_executed =>
        (pilot_auth /\ copilot_auth /\
         pilot_authorized /\ copilot_authorized /\
         time_window_open)

Init ==
    /\ pilot_auth       = FALSE
    /\ copilot_auth     = FALSE
    /\ pilot_authorized = FALSE
    /\ copilot_authorized = FALSE
    /\ release_executed = FALSE
    /\ time_window_open = FALSE

Kun TLC tarkastaa tämän mallin, se tutkii kaikki saavutettavat tilat Init-alkutiloista kaikkien mahdollisten Next-siirtymien alla. Jos jokin kelvollisten siirtymien jono voi saavuttaa tilan, jossa release_executed = TRUE turvallisuusinvariantin ollessa rikottu, TLC tuottaa vastaesimerkkijäljityksen — vaiheittaisen tilasiirtymäjonon, joka johtaa epäturvalliseen tilaan. Tämä vastaesimerkki ei ole testitapaus, joka sattui epäonnistumaan; se on todiste siitä, että määrittelyssä on aukko, ja aukko on suljettava vaatimuksissa ennen toteutuksen aloittamista.

Mitä TLA+ havaitsee, jonka testaus jättää huomaamatta, jakautuu kolmeen kategoriaan. Ensinnäkin kilpailutilanteet samanaikaisissa tilakoneissa — kaksi riippumatonta tapahtumaa, jotka voivat lomittua tavalla, jota mikään peräkkäinen testi ei voi harjoittaa. Toiseksi eloisuusrikkomukset — skenaariot, joissa järjestelmä juuttuu tilaan, joka täyttää kaikki turvallisuusinvariantit mutta ei koskaan etene kohti vaadittua tavoitetta. Kolmanneksi implisiittiset oletukset — ominaisuudet, joita suunnittelutiimi piti implisiittisinä ja siksi ei koskaan testannut, minkä TLC rikkoo tutkimalla siirtymiä, joita tiimi ei tietoisesti harkinnut.

SPARK Ada: Adan alijoukko todistettavaan oikeellisuuteen

SPARK Ada on formaalisti määritelty Ada-ohjelmointikielen alijoukko, joka on suunniteltu siten, että SPARK:lla kirjoitetut ohjelmat voidaan staattiisesti verifioida GNATprove-työkalusarjalla. SPARK rajoittaa täyttä Ada-kieltä tavoilla, jotka tekevät semantiikasta sopivan automaattiseen todistamiseen: ei aliaksia tyyppihakujen kautta (osoittimet), ei dynaamista lähetystä todistusrelevantissa alijoukossa, ei säikeistystä todistuskohteessa, ja kaikki globaali tila on deklaroitava eksplisiittisesti näkökulmamäärittein.

SPARK:n verifiointiarvo tulee kahdelta eri analyysitasolta:

Virtausanalyysi verifioi tietovirtaominaisuudet yrittämättä todistamista: se vahvistaa, että jokainen luettu muuttuja on alustettu ennen lukemista, että aliohjelmat käyttävät vain sitä globaalia tilaa, jonka ne ilmoittavat Global-näkökohdassaan, ja että tietovirrat ovat johdonmukaisia Depends-näkökohdan kanssa (joka kertoo, mitkä tulosteet riippuvat mistäkin syötteistä). Virtausanalyysi suoritetaan nopeasti — sekunneissa tai minuuteissa suurille koodikannoille — ja eliminoi kokonaisen luokan ajoaikaisia virheitä, jotka tavanomainen testaus löytäisi vain riittävällä kattavuudella.

Todistustila yrittää tyhjentää kaikki ajoaikatarkistuksen ehdot matemaattisina lauseina käyttäen GNATproven taustalla olevia SMT-ratkaisimia (Alt-Ergo, CVC5, Z3). Ajoaikatarkistusehto SPARK:ssa luodaan jokaiselle operaatiolle, joka voisi aiheuttaa ajoaikavirheen: taulukon indeksipääsyt, kokonaislukuaritmetiikka, tyyppimuunnokset, esiehtojen tarkistukset. Kun GNATprove todistaa tarkistusehdon, se on vahvistanut, ettei mikään aliohjelmasuoritus voi laukaista kyseistä ajoaikavirhettä kaikkien mahdollisten esiehdon täyttävien syötteiden osalta. Tämä on perustavanlaatuisesti vahvempi takuu kuin testaus.

-- Esimerkki: verifioitu rajoitettu puskuri C2-viestijonoon
package Message_Queue
  with SPARK_Mode => On
is
   Max_Messages : constant := 256;
   subtype Index_Type is Natural range 0 .. Max_Messages - 1;
   subtype Count_Type is Natural range 0 .. Max_Messages;

   type Queue_T is private;

   function Is_Full  (Q : Queue_T) return Boolean;
   function Is_Empty (Q : Queue_T) return Boolean;
   function Length   (Q : Queue_T) return Count_Type;

   procedure Enqueue (Q   : in out Queue_T;
                      Msg :        Message_T)
     with Pre  => not Is_Full (Q),
          Post => Length (Q) = Length (Q'Old) + 1;

   procedure Dequeue (Q   : in out Queue_T;
                      Msg :    out Message_T)
     with Pre  => not Is_Empty (Q),
          Post => Length (Q) = Length (Q'Old) - 1;

private
   type Queue_T is record
      Data  : Message_Array (Index_Type);
      Head  : Index_Type := 0;
      Tail  : Index_Type := 0;
      Count : Count_Type := 0;
   end record;
end Message_Queue;

GNATprove verifioi, että Enqueue:n ja Dequeue:n toteutus noudattaa jälkiehtojaan kaikille esiehtonsa täyttäville syötteille, eikä taulukon ulkopuolinen pääsy, kokonaislukuylivuoto tai alustamaton luku voi tapahtua. Sertifioidussa C2-sovelluksessa käytettävälle viestijonolle tämä korvaa kymmeniä raja-arvojen testitapauksia yhdellä todistuksella, joka kattaa koko syöteavaruuden.

Integrointi GNAT:iin puolustusohjelmiston CI/CD-putkessa on suoraviivaista: GNATprove käynnistetään build-vaiheena projektitiedoston määritellessä todistustason (0–4, jossa 4 yrittää korkeimman tason todistuksia). Todistustulokset lähetetään koneellisesti luettavana JSON:na, mikä mahdollistaa integroinnin virheiden seurannan ja sertifioinnin jäljitettävyyden työkaluihin.

C/C++ formaalin analyysin työkalut

Suurin osa käyttöönotetuista puolustusohjelmistoista on kirjoitettu C:llä ja C++:lla, ei Adalla. Tälle asennuskannalle kaksi formaalin analyysin työkalua on laajimmin käytetty sertifioiduissa ohjelmissa: CBMC (C Bounded Model Checker) rajoitettuun tavoitettavuustarkistukseen ja Frama-C WP-laajennuksellaan (heikoin esiehto) täyttä deduktiivista verifiointia varten.

CBMC kääntää C-ohjelmat SAT/SMT-ongelmiksi ja ratkaisee ne selvittääkseen, voidaanko tietty ominaisuus rikkoa rajoitetussa määrässä suoritusaskelia. CBMC tarkistaa natiivisti puskuriylivuodot, vapautuksen jälkeisen käytön, kokonaislukuylivuodot, nollaosoitinviittaukset ja assertoiden rikkomukset — virhekategoriat, jotka aiheuttavat suurimman osan tietoturvahaavoittuvuuksista C-koodissa. Sen tärkein vahvuus on alhainen annotointitarve: CBMC voi tarkistaa C-funktion ajoaikavirheiden varalta minimaalisilla lähdemuutoksilla. Sen tärkein rajoitus on, että se antaa takuita vain määritettyyn silmukan avausrajaan asti — rajoittamattomien silmukoiden osalta CBMC-vastaesimerkin puuttuminen ei ole todiste oikeellisuudesta.

Frama-C WP:llä on modulaarinen C-analyysikehys, joka tukee täyttä deduktiivista verifiointia ACSL (ANSI/ISO C Specification Language) -sopimusten annotoimalle C-koodille. ACSL-sopimukset määrittelevät funktion esiehdot, jälkiehdot, silmukkainvariantit ja muistijalanjäljet formaalilla kielellä, joka on upotettu C-kommentteina. WP-laajennus luo verifioinnin ehdot (VC) annotoidusta C-koodista ja tyhjentää ne Why3:n taustalla olevien todistajien avulla (Alt-Ergo, CVC5, Coq). Todistamatta jääneet VC:t edustavat joko todellisia vikoja, puuttuvia silmukkainvariantteja tai ominaisuuksia, jotka vaativat manuaalisia Coq-todistuksia.

MISRA C:n ja formaalin verifioinnin suhde on toisiaan täydentävä: MISRA C -säännöt poistavat kielen rakenteet (implisiittiset kokonaislukumuunnokset, osoittimen aliakset heittomerkkien kautta, dynaaminen muistinvaraus), jotka tekevät C-koodin semantiikasta monitulkintaisen ja siten vaikean verifioida formaalisti. MISRA C:2012 -vaatimustenmukaisuuden noudattaminen — erityisesti pakollisten sääntöjen osalta kategorioissa Osoitintyyppien muunnokset, Päällekkäinen tallennus ja Oleellinen tyypimalli — luo hyvin määritellyn semanttisen perustan, jonka Frama-C:n WP-analyysit vaativat tuottaakseen vankat tulokset. MISRA C -vaatimustenmukaisuustarkistus on siis oikea ensimmäinen vaihe ennen Frama-C:n soveltamista, ei vaihtoehto sille.

Työkalu	Tekniikka	Annotointitarve	Takuun vahvuus	DO-330 TQL
CBMC	Rajoitettu mallintarkistus (SAT)	Alhainen	Rajaan asti	TQL-3 (täydentävä)
Frama-C / WP	Deduktiivinen verifiointi (SMT)	Korkea (ACSL-sopimukset)	Täysi (todistetut tavoitteet)	TQL-1 (kvalifiointisarjalla)
Polyspace Verifier	Abstrakti tulkinta	Alhainen–kohtalainen	Vahva (voi yliarvioida)	TQL-1 (kvalifiointisarja saatavilla)
GNATprove (SPARK)	Deduktiivinen + virtausanalyysi	Korkea (Ada+SPARK-sopimukset)	Täysi (todistetut tavoitteet)	TQL-1 (kvalifiointisarja saatavilla)

Mallintarkistus protokollan verifiointiin

Mallintarkistus tutkii kattavasti äärellistilaisen mallin tilaavaruuden selvittääkseen, pitääkö temporaalilogiikan ominaisuus kaikissa saavutettavissa tiloissa. Puolustuksen C2-protokollille — todennushandshake-kättelyille, viestin sekvensoinnille, linkkitilan konvergenssille, kryptografisen protokollan oikeellisuudelle — mallintarkistus on suorin tie varmuuteen, koska protokollan käyttäytyminen on luonteeltaan samanaikainen ja vikamuodot ovat juuri niitä lomituksesta riippuvaisia vikoja, joita testaus ei luotettavasti paljasta.

Perustavanlaatuinen haaste on tilaräjähdys: tilaavaruuden koko kasvaa eksponentiaalisesti samanaikaisten komponenttien lukumäärän myötä. C2-järjestelmässä, jossa on 8 solmua ja kussakin 16 tilabittiä, on teoreettinen tilaavaruus 2^128 — noin 3,4 × 10^38 tilaa, jota mikään eksplisiittitilainen mallintarkistaja ei voi luetella äärellisessä ajassa. Puolustusohjelmat käsittelevät tilaräjähdystä neljällä toisiaan täydentävällä strategialla:

Abstrahointi. Korvataan konkreettiset data-arvot abstrakteilla domeeneilla, jotka säilyttävät tarkistettavat ominaisuudet. Sen sijaan, että mallinnettaisiin 32-bittinen järjestysnumero, mallinnetaan se abstraktina elementtinä järjestetyssä joukossa {INITIAL, NEXT, WRAP}, joka kuvaa sekvensoinnin semantiikan koko numeerista aluetta käyttämättä. Vastaesimerkillä ohjattu abstraktion tarkentaminen (CEGAR) automatisoi tämän: mallintarkistaja tarkentaa abstraktiota aina, kun se tuottaa vastaesimerkin, joka on toteutumaton konkreettisessa mallissa.

Symmetrian vähentäminen. Hyödynnetään rakenteellisia vastaavuuksia komponenttien välillä. Jos 8 solmua C2-verkossa on rakenteellisesti identtisiä, mallintarkistajan tarvitsee tutkia vain yksi edustaja kustakin järjestelmätilojen ekvivalenssiluokasta 8 solmun permutaatioryhmän alla. Tämä voi vähentää efektiivistä tilaavaruutta kertoimella N! (8! = 40 320 kahdeksalle solmulle).

Osittainen järjestyksen vähentäminen. Monet samanaikaiset suoritukset, jotka eroavat vain riippumattomien tapahtumien järjestyksessä (tapahtumat, jotka eivät jaa tilaa), johtavat samaan tilaan. Osittaisen järjestyksen vähentäminen tiivistää nämä vastaavat järjestykset yhdeksi edustajaksi ilman ominaisuuksien tarkistuksen kattavuuden menetystä.

Rajoitettu mallintarkistus. Sen sijaan, että tutkittaisiin kaikki mielivaltaisen pituiset polut, tarkistetaan kaikki k:ta lyhyemmät polut SAT- tai SMT-ratkaisijalla. Useimmat protokollaviat ilmenevät lyhyissä vastaesimerkkijäljityksissä (4–20 askelta); rajoitettu mallintarkistus k=30:lla löytää suurimman osan protokollabugeja, kun taas pysyy laskennallisesti hallittavissa.

Kun mallintarkistaja löytää ominaisuusrikkomuksen, se tuottaa vastaesimerkkijäljityksen — täydellisen järjestelmätilojen jonon alkutilasta rikkovaan tilaan. Tämä jäljitys on suoraan toimiva: se määrittää täsmälleen, mitkä tapahtumajonot johtavat epäturvalliseen tilaan, mikä mahdollistaa kehittäjien toistaa virheen deterministisesti ja suunnitella protokollakorjauksen. Yhdessä dokumentoidussa puolustuksen C2-protokollan verifiointitapauksessa 12-askelinen vastaesimerkkijäljitys paljasti, että todennuksen ohittaminen oli mahdollista, jos tietty sanomavaiveen ja uudelleenlähetyksen yhdistelmä tapahtui — skenaario, jota 18 kuukauden integraatiotestaus ei ollut harjoittanut.

Formaalien menetelmien integrointi DO-178C-vaatimustenmukaisuuteen

DO-178C:n DO-333-lisäys luo kehyksen formaalien menetelmien käyttämiselle vaihtoehtoisten vaatimustenmukaisuuden osoittamiskeinojen tiettyihin DO-178C-verifiointitavoitteisiin. DO-333:n käyttö edellyttää Formaalien menetelmien suunnitelmaa, jossa käsitellään:

• Valittu formaali menetelmä (tai menetelmät) ja sen valinnan peruste
• Formaalisti verifioitavat ominaisuudet ja niiden kartoittaminen DO-178C-ohjelmistovaatimuksiin
• Käytettävät työkalut, niiden DO-330-kvalifiointistatus ja kvalifiointisuunnitelma, jos ei ennalta kvalifioitu
• Miten formaaliverifiointinäyttö esitetään ohjelmiston saavutusyhteenvedossa
• Mikä formaalin verifioinnin ja testauksen yhdistelmä saavuttaa täydellisen tavoitekattavuuden

Jäljitettävyys on kriittinen integrointimekanismi. DO-178C:n jäljitettävyysketju kulkee järjestelmävaatimuksista korkean tason vaatimusten (HLR), matalan tason vaatimusten (LLR), lähdekoodin ja verifiointitapausten kautta. Formaalien artefaktien on liityttävä tähän ketjuun määritellyissä pisteissä:

Järjestelmävaatimus (SRD)
    └─► Korkean tason vaatimus (HLR)  ◄── TLA+-määrittelyn ominaisuudet
            └─► Matalan tason vaatimus (LLR) ◄── SPARK-sopimukset / ACSL-annotaatiot
                    └─► Lähdekoodi  ◄── GNATprove / CBMC / Frama-C -kohde
                            └─► Verifiointitapaukset (SVCP/SVR)
                                    └─► Todistusraportit, mallintarkistajan tulosteet,
                                        vastaesimerkkivapaat verifiointiloki

Työkalujen kvalifiointi DO-330:n mukaisesti on toinen integrointihaaste. Työkalu, joka poistaa vaaditun DO-178C-verifiointiprosessin — kuten formaali todistaja, joka poistaa rakenteellisen kattavuuden testauksen tarpeen — on kvalifioitava TQL-1-tasolla. TQL-1-kvalifiointi vaatii Työkalujen kvalifiointisuunnitelman, Työkalujen saavutusyhteenvedon, Työkalujen operatiiviset vaatimukset ja testitodisteet, jotka on luotu ohjelman build-ympäristössä. AdaCoren (GNATprove), MathWorksin (Polyspace) ja LDRA:n ennalta kvalifioidut työkalupakettit vähentävät tätä vaivaa huomattavasti verrattuna talon sisäiseen kvalifiointiin, mutta ohjelman on silti varmistettava, että toimittajan kvalifiointi soveltuu heidän tiettyyn työkaluversiooonsa ja käyttökontekstiinsa.

Tekoälyn etiikka sotilaisjärjestelmissä on yhä relevantimpi aihe, kun ohjelmat harkitsevat tekoälyavusteista formaalia verifiointia — työkaluja, jotka käyttävät neuroverkkoja ehdottamaan silmukkainvariantteja tai todistusstrategioita. Tällaisten tekoälyavusteisten ehdotusten sertifiointistatus on ratkaisematta nykyisen DO-178C-ohjauksen puitteissa; ohjelmien tulisi käsitellä tekoälyavusteisia ehdotuksia siten, että ne vaativat itsenäisen ihmisen tarkastelun ennen sisällyttämistä sertifiointinäyttöön.

Kustannus-hyötyanalyysi: milloin formaali verifiointi kannattaa

Formaalin verifioinnin kustannus on todellinen ja huomattava. 10 000 rivin SPARK Ada -moduulin annotoiminen täydelliseen ajoaikavirheiden todistukseen vaatii 3–6 kuukautta asiantuntijainsinöörityötä. Formaalin verifiointityökalun kvalifiointi DO-330 TQL-1 -tasolla vie 3–6 kuukautta lisävaivaa ensimmäisellä kerralla. TLA+-määrittelyn kirjoittaminen ja tarkistaminen monimutkaiselle protokollalle vie viikkoja. Mikään näistä kustannuksista ei katoa.

Hyötyjen laskenta on tehtävä oikeaa vaihtoehtoa vastaan. Vaihtoehto formaalille verifioinnille DO-178C Taso A:lla ei ole ei verifiointia; se on kattava testaus MC/DC-kattavuuteen, mikä kompleksiselle tilakoneelle, jossa on N ehtoa päätöksessä, vaatii O(2N) testitapausta, mahdollisesti myös formaalin analyysin MC/DC-riittävyyden osoittamiseksi. Ei-triviaalien turvallisuuskriittisten funktioiden osalta Taso A -tavoitteiden saavuttamisen testauksen kustannukset ilman formaaleja menetelmiä ovat usein korkeammat kuin formaalin verifioinnin kustannukset — ja tarjoavat heikomman varmuuden muodon.

Alan data tukee johdonmukaisesti kolmea johtopäätöstä:

Vikojen löytämiskustannus. Formaalin määrittelyn aikana löydettyjen vikojen korjauskustannus on noin 1×. Koodikatselmusten aikana löydettyjen vikojen korjauskustannus on 10× perustasosta. Integrointitestauksen aikana löydettyjen vikojen korjauskustannus on 100×. Sertifioinnin jälkeen löydettyjen vikojen korjauskustannus on 1 000× tai enemmän, mukaan lukien uudelleensertifioinnin lisäkustannukset. Formaalilla määrittelyllä, joka paljastaa viat mahdollisimman varhaisessa vaiheessa, on paras vikakustannusprofiili kaikista tekniikoista — erityisesti arkkitehtuuritason vioille (virheellinen tilakoneen suunnittelu, protokollan kilpailutilanteet), joiden löytämisessä formaalit menetelmät ovat ainutlaatuisen tehokkaita.

Elinkaaren verifiointikustannuksen vähentyminen. Ohjelmissa, jotka soveltavat SPARK Adaa Taso A -komponentteihin, verifiointikustannusten lasku on 50–70 %. Formaali todistaja tyhjentää rakenteellisen kattavuuden tavoitteet, jotka muuten vaatisivat laajan testirunkojen kehittämisen, kattavuuden instrumentoinnin ja kattavuuden mittaamisen kombinatorisessa testausmatriisissa.

Milloin formaali verifiointi ei kannata. DO-178C Taso C:n tai sen alapuolella olevalle ohjelmistolle sekä MIL-STD-882 Kategoria III:n tai IV:n osalta formaalien menetelmien ylimääräinen työ ylittää tyypillisesti hyödyn. Taso C vaatii 100 % lause- ja päätöskattavuutta — saavutettavissa tavanomaisilla testivetoisen kehityksen käytännöillä ja kattavuustyökaluilla. Formaalien menetelmien soveltaminen Taso C:lle lisää kustannuksia ilman suhteellista varmuuden lisäystä. Tekninen harkinta on suoraviivainen: sovella formaaleja menetelmiä siellä, missä sääntelyvaatimukset pakottavat sen (Taso A, Taso B monimutkaisille tilakoneille) tai missä havaitsemattomien vikojen seuraukset — hengen menetys, järjestelmän vikaantuminen taistelussa — oikeuttavat investoinnin sääntelyvelvoitteesta riippumatta.

Käytännön polku useimmille puolustusohjelmille on kerrostunut lähestymistapa: TLA+-formaali määrittely kaikille turvallisuuskriittisille tilakoneille ja protokollille; SPARK Ada uusille tai uudelleenkirjoitetuille Taso A -komponenteille; CBMC ja MISRA C olemassa oleville C-komponenteille, joita ei voi kirjoittaa uudelleen; ja Frama-C/WP kaikkein kriittisimmille C-funktioille, joissa täysi deduktiivinen verifiointi on perusteltua. Jokainen kerros lisää varmuutta pelkän testauksen ylittäen, ja jokaisen kerroksen tuloste luo sertifiointinäyttöä, joka vähentää testaustarvetta komponentti- ja integrointitestaustasolla.