VIPER-mikroprocessorchipet är ett av resultaten av ett forskningsprogram om högintegrity computing som genomförs vid Royal Signals och Radar Etablering i Malvern, England. RSRE (som är en forskningsstation som tillhör det brittiska försvarsministeriet) har utvecklat formella metoder för att specificera och analysera programvara i omkring 15 år, men först 1983 började vi titta på det lika utmanande problemet med datorutrustning. Korrekt datorutrustning har bara blivit ett problem på grund av trycket från datoranvändare (civila och militära) att sätta programmerbar elektronik i allt mer kritiska system. De medicinska, fordons- och avioniska samhällena använder nu alla allmänna mikroprocessorer i system som skulle kunna utsätta sina kunders liv för fara, och tröskeln pressas ständigt högre: datorstyrning erbjuder så många fördelar i kostnad, prestanda och flexibilitet att dess frestelser sällan kan motstås. Konventionella mikroprocessorchips är dock varken tillräckligt väl specificerade eller tillräckligt noggrant implementerade för livskritiska (eller säkerhetskritiska) tillämpningar. Varje månad ser en annan pressrapport om problem i allmänt använda enheter. VIPER, liksom FM8501 och 8502, föddes av behovet av en mikroprocessor med en exakt, formell, specifikation, högsta möjliga försäkran om att den fysiska enheten överensstämmer med den, och de särskilda egenskaper som krävs för hög integritet applikationer. Computational Logic Incorporated fick i uppdrag av NASA att granska arbetet med VIPER, under en långvarig ram för samarbete inom flyg- och rymdforskning mellan NASA och Royal Aerospace Etablering i Storbritannien. Information om VIPER tillhandahölls av oss själva och av Marconi Electronic Devices Ltd. VIPER utvecklades som svar på ett antal brittiska militära krav. Vi fattade ett tidigt beslut ( 1984) att tillverka chips som en demonstration av vad som kunde göras, och därför begränsade vi oss till teknik som erbjöd en relativt snabb väg till kisel. Gordons LCF-LSM-system (som nu har mognat till HOL, se referenser i slutet av rapporten) var det självklara valet, eftersom en fullständig redovisning av det hade publicerats med en handledning exempel på maskinvaruverifiering - en enkel & bit maskin som nu kallas "Tamarack". HOL är syntaktiskt ganska lik hårdvarubeskrivningsspråket ELLA, så vi bestämde oss för att leva med ett informellt (men tekniskt enkelt) steg i designprocessen genom att byta språk i mitten. Ett starkt formulerat språk som HOL är till stor hjälp vid skrivandet av en specifik handling (den upptäcker en stor del av felen) och ett teoremtest för den finns tillgängligt. ELLA är en etablerad HDL med en mängd verktyg, några *Detta arbete stöddes delvis på Computational Logic, Inc. av NASA Langley Research Center genom Defense Advanced Research Projects Agency, ARPA Order 584155. De åsikter och slutsatser som finns i detta dokument är författarnas och bör inte tolkas som att representera den officiella politik, antingen uttryckt eller underförstådd, av Computational Logic, Inc., NASA, Defense Advanced Research Projects Agency eller US regering. CH3033-8~91~0000-0091$01.OO 0 1 9 9 1 IEEE 91 av vilka kan r e h e en block-nivå beskrivning i en grind-nivå design med nästan ingen mänsklig intervention. Vi ändrade vid minsta ansträngning; processen kunde lätt mekaniseras men för en enhet så enkelt som VIPER detta verkade inte värt tid. Från språket förändras nedåt, VIPER designen var knytnäve verifieras av en process av "intelligent uttömmande simulering" vars täckning beror på vilken uppsättning av testvektorer tillämpas. Dessa vektorer (som innehåller "inte bryr sig" i profusion) genereras av ELLA-simulatorn från ett handskrivet program. Även om vi tror att denna metod är sund (den är i själva verket pessimistisk: den förkastar vissa korrekta kretsar men bör aldrig acceptera en fel en) det beror alltför mycket på mänsklig assisuity för komfort, så vi har ersatt den. Den nya tekniken, utvecklad av Clive Pygott vid RSRE och baserad på arbetet av R. E. Bryant, kallas NODEN; den användes i augusti 1989 för att upprepa den låga nivån verifiering av den senaste versionen av VIPER. Denna enhet (VIPER 1 A ) är utformad för att fungera i par och har inbyggda jämförelsen för att kontrollera adress och data buss fel. Jämförelsepunkterna har för många ingångar för att NODEN-analysatorn ska kunna kontrollera dem, men resten av konstruktionen bekräftades vara korrekt. De övre nivåerna av verifieringen gjordes av Avra Cohn vid University of Cambridge i England med hjälp av HOL Theorem Prover. Beviset är inte komplett på ett antal områden som rör betydelsen av datoraritmetik. Dessa punkter har dokumenterats av Cohn själv och kommenteras ytterligare i denna rapport. Vi är övertygade från noggranna (men informella) argument, simulering, och testning av faktiska marker att genomförandet är korrekt, men som Fetzer [l2] och andra har påpekat är det inte motiverat i strikt matematiska termer att hävda en "säker" av någon fysisk anordning. Hårdvara, av något slag, skiljer sig i grunden från datorprogramvara genom att ett verkligt formellt bevis (en "demonstration" i Fetzers termer) på korrekthet inte är möjligt. Fysiska enheter slits ut och bryts ner, och ingen mängd formell logik kan garantera immunitet: i slutändan fysik gör sina egna regler. Med VIPER har vi lagt ner nästan lika mycket arbete på att skydda mot hårdvarunedbrytning (med hjälp av paritetsbitar, master / slavdrift, inbyggd test och självtestbar logik) som på att säkerställa korrekt design. De två aspekterna är naturligtvis kompletterande, eftersom de flesta överflödiga system byggs runt antagandet att kanalerna kommer att misslyckas självständigt. Om det finns ett vanligt konstruktionsfel, kan de alla misslyckas tillsammans. Denna rapport och Avra Cohns arbete bekräftar vårt intryck av att mer återstår att göra, både för att bygga upp förtroendet för den befintliga VIPER-designen och för att utveckla nya tekniker för design och verifiering som undviker de nuvarande metodernas begränsningar. CLI själva är stora bidragsgivare till detta område; i Storbritannien sponsrar vi arbete med metoder för att förfina en funktionell specifikation genom att korrekt bevara omvandlingar, så att den slutliga gate-nivådesignen är "korrekt genom konstruktion". Testfordonet för detta arbete kommer troligen att vara en mycket snabbare (men uppåtkompatibel) utveckling av VIPER. På kiselnivå försäkrar vi oss mot fel i CAD-programvaran och tillverkningsprocessen (som ligger under slutet av vårt verifieringsarbete) genom att sponsra en andra, oberoende, gate-nivå design av chipet med hjälp av en annan teknik. På längre sikt anser vi att en kombination av metoder vanligtvis kommer att behövas för att uppnå högsta möjliga säkerhet. En konstruktion kan uttalas "korrekt genom konstruktion" av en felaktig programvara verktyg; att skydda mot -9 2 visat sig genomföra sin topp-nivå specifikation (instruktionstolken). Detta är inte en unik ståndpunkt, utan en av Cambridge Universitys konsulter har nyligen kommit fram till en liknande slutsats [4]. Avsnitt 2 innehåller en informell beskrivning av VIPER microprc+ cessor. Analysen av VIPER börjar i avsnitt 3 med en kontur av de abstrakta skikt som används för att ange VIPER. Avsnitt 4 omfattar vart och ett av bevisen och försök till överensstämmelse mellan nivåerna i specifikationen. Ett schematiskt blockdiagram över innehållet i avsnitten 3 och 4 visas som figur 1. Slutsatsen innehåller en diskussion om några av de bredare frågorna i hanteringen av formella hårdvaruverifieringsprojekt, med hjälp av VIPER-projektet som exempel. I hela rapporten jämför vi den specifikation och verifieringsmetod som används för VIPER med den som används under specifikationen och verifieringen av mikroprocessorn FM8502 [25].
I REF rapporteras "ett fåtal" fel i specifikationen och två diskuteras i detalj.
Report on the formal specification and partial verification of the VIPER microprocessor
{'venue': "COMPASS '91, Proceedings of the Sixth Annual Conference on Computer Assurance", 'journal': "COMPASS '91, Proceedings of the Sixth Annual Conference on Computer Assurance", 'mag_field_of_study': ['Computer Science']}