Mötesanteckningar Inga-Lill Bratteby-Ribbing, FMV: KC Ledstöd (018-120263, inga-lill.bratteby-ribbing@fmv.se)

IG Programvarusäkerhet: Möte # 5, 03-10-21

Antal mötesdeltagare: f.m.: 8, e.m.: 26 (se medlemslista).

Gruppmöte
1

Synpunkter på hemsidan (http://sesam.tranet.fmv.se, se under Arbetsgrupper)
IG:s hemsida är nu färdig i sin struktur i o m inlägg av arvet från FoTA P12, nytt material från IG:et samt uppdateringar betr. aktuella kurser o verktyg, vilket gett –tack vara insatser från Ingemar Johansson, Anna Kåsjö o ordf– en bra struktur med mycket matnyttigt innehåll. Inga förändringar föreslogs (frånsett inkludering av rubriken ”Metoder”).

2

SCR-verktyg bl a för tabellorienterad specning av programvarukrav, Inga-Lill Bratteby-Ribbing.
En integrerad uppsättning verktyg, Software Cost Reduction, har utvecklats på NRL (Naval Research Laboratory) –en vidareutveckling från 70-talet o framåt av bl a Parnas A-7/SCR kravspecning, CoRE (från Sw Production Team) samt NRL:s formella modellarbete. Specar uttrycks i en tabellorienterad notation (jmf SpecTRM, vars logiska and-or-tabeller i SCR motsvaras av en enda tabell). Verktyg finns som verifierar dessa genom konsistenskontroll (m a p missade fall, ickedeterminism, cirkulära beroenden) samt simulering av systemets beteende (genom att exekvera specarna). Specarna kan även verifieras m h a formella verktyg

Model checker” (avsedd att utvidgas dels med en simulator för generering av motexempel –som stöd för felanalyseringen, dels med automatgenererade abstraheringar –för att bemöta problemet tillståndsexplosion)
Theorem prover” (vars användning kräver djupare formell skolning, o som därför är kompletterad dels med
- TAME, ett användarvänligt gränssnitt mot det formella bevisverktyget/språket PVS prover, dels med en
- Invariantgenerator som stöd i bevisföringen)
Property checker” (Salsa)
Testfallsgenerator (som utgår från specarna)
Källkodsgenerator (som –givet korrekt– eliminerar verifieringsbehovet från spec till kod)

En verktygsprovning o jämförelse med SpecTRM vore intressant. Ordf har kontaktat chefsarkitekten för SCR.

3

Idéer fortsatt verksamhet - Diskussioner
Kommande möten: Se punkten övrigt.
Windows XP: Redan för drygt 1 år sedan diskuterades över nätet vådan av Microsofts möjlighet att utan användares vetskap automatiskt kunna uppdatera installerat OS (se www.infoworld.com/articles/op/sml/02/09/16/020916opwinman.xml).
Under detta år har även en artikel över XP:s kontroversiella egenskaper sammanställts (http://www.hevanet.com/peace/microsoft.htm). Inte bara oåtgärdade, kända blottor hör till problemen, utan även dolda kopplingar genom användares brandvägg, svårigheter att kunna nyttja viss funktionalitet eller få senaste uppdatering utan att vara uppkopplad på nätet. Ur diskussioner med Praxis grundare på senaste SafeComp-konferensen (o dennes kontakter med Intel) framkom även, att Intels microkod kan uppdateras av Microsoft’s produkter utan användares vetskap (framgår ev. ur www.intel.com). Konsekvenserna utgör hot såväl ur IT-Säkerhets- som Systemsäkerhetssynpunkt.

4

Övrigt

Anders Edbom, som ersätter Anders Wahlström från SBD, hälsades välkommen som ny medlem.
Kockums undersöker möjligheter till prov av SpecTRM.
Nästa möte: 2004-02-12. Tema: UAV:er. Programkommitté: Koberstein, Tengroth, ordf.

Aktivitetslista IG Programvarusäkerhet
Nr
Klar till
Ansvarig
Mötesnotiser senaste möte (#5)
5.1
031031
Ordf
Förberedelser av presentationer nästa möte 5.2 040131 TBD
Förnyade kontakter med NRL 5.3 031231 Ordf
Dagordning möte #6 (feb 2004)
4.4
040115
Ordf, Björn K, Johan T
Exempel på krav ej uttryckbara i SpecTRM 4.5 031021 Medl
Komplettering av # 3.2 med företagsspecifika frågeställningar
3.3
030917 
Deltagare 
Kompletteringsförslag till hemsida (verktyg, utb etc)
1.5
030330
IG-medl
Egen applikation strippad för verktygsprov
1.8
030409
IG-medl