Author:
Mariëlle Stoelinga is universitair hoofddocent risicomanagement van ICT aan de Universiteit Twente. Bij de afgelopen QEST-conferentie was zij medevoorzitter van de programmacommissie.
Reading time: 4 minutes
Mariëlle Stoelinga van de UT ging naar QEST-conferentie en tekende de trends op in systeemontwerp en -analyse: security op codeniveau, peer-to-peercommunicatie en software verspreid over multi-administratieve domeinen.
Wat zijn de nieuwe ontwikkelingen in design en analyse van niet-functionele eigenschappen zoals beveiliging, performance en resourcegebruik? Toonaangevende conferentie op dit gebied is QEST (Quantitative Evaluation of Systems). De tiende editie was van 27 tot en met 30 augustus in de Argentijnse hoofdstad Buenos Aires.
Traditioneel brengt QEST de meer praktisch georiënteerde onderzoekers aan performance(metingen) samen met de meer theoretische researchers op het gebied van modellering en analyse. Deze brug slaan is niet altijd gemakkelijk omdat beide kampen hun eigen terminologieën en voorkeuren hebben. Toch is het deze kruisbestuiving die de conferentie zo interessant en innovatief maakt.
Accuraat
Spectaculair was de keynote van Gilles Barthe. De onderzoeker van het IDMEA Sofware Institute uit Madrid presenteerde de tools Easycrypt en Certicrypt om automatisch securityeigenschappen te checken op codeniveau. In het bijzonder heeft hij hiermee de correctheid aangetoond van RSA-OAEP, een variant van RSA waarvan de correctheid al vijftien jaar een onopgelost probleem was. Hoewel Barthes techniek nog redelijk wat domeinkennis vergt vanwege de speciale taal waarin de te verifiëren securityeigenschappen moeten worden gespecificeerd, valt hier de komende jaren veel van te verwachten. Code-level security is een notoir lastig probleem en de gepresenteerde resultaten zijn bijzonder hoopvol.
In een andere keynote sprak Edmundo de Souza e Silva van de Universidade Federal do Rio de Janeiro over het ontwerp van peer-to-peer swarming systems, bedoeld om contentfiles te verspreiden over een grote hoeveelheid gebruikers. Voorbeelden zijn Bittorrent, het Linux-distributiesysteem en video-on-demand-oplossingen. Deze hakken grote bestanden op in kleine stukjes, die ze vervolgens over meerdere (meestal willekeurig geselecteerde) hosts verspreiden. Dit verhoogt niet alleen de performance (load balancing), maar ook de beschikbaarheid; doordat content op meerdere plaatsen staat, is het systeem robuuster tegen uitval van hosts.
Probleem hierbij is dat impopulair materiaal zich niet goed verspreidt, terwijl de totale hoeveelheid van niet-populaire content toch hoog is. Dit wordt nog versterkt als slechts een deel van een file impopulair of zeldzaam is. De Souza e Silva presenteerde verschillende oplossingen voor dit probleem, waaronder mechanismen om populaire en impopulaire content te bundelen en om bandbreedte onder verschillende peers anders te verdelen.
De award voor het beste paper ging naar Luca Bortolussi van de universiteit van Triëst en Guido Sanguinetti van de universiteit van Edinburgh voor werk op het gebied van machine learning. Dit is een innovatieve techniek om automatisch een systeem- of designmodel te synthetiseren uit data, bijvoorbeeld systeemlogs. Het heeft de afgelopen jaren een hoge vlucht genomen in een scala aan toepassingen, waaronder modelgebaseerd testen, automatische spraakherkenning en datamining. Het prijswinnende paper van Bortolussi en Sanguinetti behandelt een methode om automatisch kansmodellen te leren en te ontwerpen uit constraints. Dit maakt het mogelijk om sneller betere modellen te verkrijgen, omdat in het model aanwezige parameters, bijvoorbeeld waarden van verwachte aankomst- of servicetijden, heel snel en accuraat uit systeemlogs of traces zijn te extraheren.
Nederlandse bijdrages waren er in Buenos Aires van David Jansen van de Radboud Universiteit Nijmegen en Dennis Guck van de Universiteit Twente. Jansen pleitte ervoor om niet te vragen of een systeem aan de requirements voldoet, maar in hoeverre. Dit vergemakkelijkt trade-offs tussen verschillende implementaties en verschillende vereisten. Zijn wetenschappelijke bijdrage is een methode die als het ware de afstand meet tussen implementatie en specificatie. Guck presenteerde een tool voor de analyse van Markov-automaten, een nieuw en krachtig model voor stochastische analyse dat snel aan populariteit wint, onder meer omdat het accuratere methodes geeft voor foutboomanalyse, errormodellen en performance.
Krachtig
Een belangrijk onderdeel van QEST vormen de tooldemonstraties. Barbara Kordy van de universiteit van Luxemburg gaf een heldere presentatie van ADTool. Hiermee zijn securityscenario‘s in attack/defence trees door te rekenen en hun kosten, kansen, risico‘s en impact te bepalen, als ook het effect van tegenmaatregelen.
Agung Julius van het Rensselaer Polytechnic Institute nam het gehoor mee naar Strong, een Matlab-toolbox voor zogeheten hybride modellen. Deze kenmerken zich door de combinatie van continu gedrag (zoals temperatuur, snelheid en luchtdruk) en discreet gedrag (aan/uit van een thermostaat, vooruit/achteruit bij een motor). In automotive- en aerospacetoepassingen zijn ze reeds gemeengoed, bijvoorbeeld om een cruisecontrol of luchtvaartbewegingen door te rekenen. De Strong-toolbox biedt features op het gebied van coverage, modelconsistentie en simulatie van trajectory‘s en robuustheid.
Een andere belangrijke tool is de statistische model-checker Plasma Lab, in ontwikkeling bij Inria in Rennes. Dergelijke gereedschappen bieden de gezamenlijke voordelen van model-checking en simulatie: zowel de modelleringstalen als de te verifiëren eigenschappen zijn afkomstig uit model-checkers, en dus krachtig, terwijl de analysetechnieken uit de systeemsimulatie komen, en daarom ook krachtig en snel zijn. Statische model-checkers combineren dan ook het beste uit deze werelden.
