Statisk kodanalys letar fel i programkoden utan att exekvera den. Tekniken har använts sedan 70-talet och i takt med att programmen blivit komplexare har området blivit allt hetare för säkerhetskritiska tillämpningar som bilar, flygplan, rymdraketer, kraftverk och medicintekniska apparater.

Synopsys och Mathworks har exempelvis köpt universitetsavknoppningarna Coverity och Polyspace för stora belopp och så sent som i februari adderade uppsaliensiska IAR statisk kodanalys i Embeddeed Workbench.

Att det finns ett behov av bättre testverktyg inklusive statisk analys är helt klart. Runt en tredjedel av kostnaden för mjukvaruutveckling utgörs av testning och ändå är det många fel som slinker igenom.

– Dagens verktyg för statisk analys är inte särskilt intelligenta men utökas ibland med diverse extra verktyg. Dessutom saknar de den skalbarhet som finns i vår ansats. De är också kostsamma, en enda licens kan gå på 360 000 till 480 000 kronor per person och år, utan testverktyg och liknande, säger Johan Glimming som grundat Functor tillsammans med Paul Subotic.

Företaget har påbörjat resan från forskning till kommersiell verksamhet genom att förpacka resultat från svenska och brittiska universitet så att de ska bli praktiskt användbara.

Det är inte helt lätt att hänga med när Functors teknikchef Johan Glimming börjar förklara hur Prevent och Scalor kan revolutionera testningen, men vi gör ett försök.

Scalor är ett metaspråk men att få världen att ta till sig ett nytt språk är näst intill omöjligt. En bättre väg är att förpacka Scalor så att det kan testa program skrivna i något existerande språk. Det är exakt vad Prevent gör.

– Prevent förhindrar dålig kod och gör programmerare skickligare genom olika typer av feedback-loopar, säger Johan Glimming.

Prevent pluggas in som ett nytt lager i verktygskedjan och fungerar oberoende av verktygen. Det är snabbt och kan generera många av testfallen automatiskt.

Verktyget letar efter logiska fel, som att man använder en variabel som inte definierats, skickar in 12 bitar långa data när det ska vara 10 bitar eller upptäcker om det uppstår minnesläckage.

Resultatet blir en rapport som beskriver hur korrekt koden är i termer av fel som behöver åtgärdas eller vilka andra tester som kan behöva göras.

Functor har arbetat med produktifieringen av Prevent under ett antal år och i planerna finns att verktyget ska certifieras enligt standard för testverktyg till säkerhetskritiska system.

– Vi hade kunnat hindrat Heartbleed. Vi isolerade fixen och den är rakt spot-on vad vår produktionsversion av Prevent klarar automatiskt, säger Johan Glimming.

Säkerhetshålet som döptes till Heartbleed lämnade massvis av webbsidor med SSL-kryptering vidöppna. Felet upptäcktes för ett knappt år sedan, trots att det exi­sterat sedan 2011. Hur stor skada det skapade och hur många timmar det gick åt för att uppgradera är det ingen som med säkerhet kan säga, men väldigt många sajter låg vidöppna för attacker.

– Vi har kört Prevent på Erlang OTP, GNU Ada kompilatorn, BLAS, OpenBLAS och MySQL. På embeddedgrejer som Atmel Software Framework 3.21 och Microchip code libraries liksom på multicore-grejer som Nvidias bibliliotek för CUDA.

Prevent sägs kunna hitta över
50 procent av felen, gäller det alla typer av fel?

– Nej! Det gäller specifikt projekt som har mycket minnesintensiva operationer eller operationer på arrays såsom grafikprogram och annat.

Verktyget är ännu inte moget att sättas i händerna på kunderna så Johan Glimming konsultar åt de företag som vill testa det. Det gäller exempelvis en brittisk kraftkoncern som driver kärnkraftverk.

Grunden i Prevent är Scalor, ett metaspråk som i sig förbjuder programkod som i andra programspråk skulle leda till buggar. Både testning, statisk kodanalys, formell verifiering och modellverifering, finns inbyggt i själva språket. När ditt program är godkänt av kompilatorn, kan du bocka av de övriga punkterna – utan att ha behövt ta hjälp av verktyg från företag som Rational, Coverity, Intel, Mathworks Prover, och andra.

Scalor innehåller en bevismotor av typen SMT (Satisfiability Modulo Theories).

Kan du mycket enkelt beskriva vad Scalor är?
– Scalor är ett metaspråk som automatiskt kan göra avancerad statisk analys och modellera naturliga språk, domänspecifika språk och automatiskt statiskt garantera egenskaper och göra jobb som annars kan ge spaghettikod och kostsamma run-time checks. Scalor löser det jag kallar det semantiska gapet. Istället för att generera kod och köra statisk analys gör vi statisk analys redan i modellen självt. Då försvinner det semantiska gapet.

Scalor har potential att göra program mer energieffektiva eftersom mycket av beräkningarna flyttas till kompileringen, istället för att utföras under exekveringen.

– Samtidigt kan vi parallellisera programmen mer. Det är en av fördelarna i funktionell programmering. Detta är idealiskt för multicore, säger Johan Glimming.