ITEM METADATA RECORD
Title: Static and Dynamic Verification of Indirect Data Sharing in Component-Based Applications (Statische en dynamische verificatie van het indirect delen van data in componentgebaseerde toepassingen)
Other Titles: Static and Dynamic Verification of Indirect Data Sharing in Component-Based Applications
Authors: Desmet, Lieven
Issue Date: 9-Jan-2007
Abstract: Moderne softwaresystemen worden steeds frequenter opgebouwd als composities van herbruikbare componenten. Dergelijke componentgebaseerde software promoot vaak eenvoudige syntactische interfaces om het bouwen van nieuwe composities zo eenvoudig mogelijk te maken. Hoewel deze componenten op syntactisch niveau gemakkelijk samen te stellen zijn tot nieuwe composities, blijken losgekoppelde componenten echter regelmatig semantisch van elkaar af te hangen. Dit is onder andere het geval bij composities met een gemeenschappelijke opslagplaats (shared repository) via dewelke componenten indirect data met elkaar kunnen delen. Typisch worden deze verborgen afhankelijkheden niet gecontroleerd tijdens de compilatie, en op die manier leiden inbreuken op deze afhankelijkheden in huidige softwaresystemen tot fouten tijdens de uitvoering.De hoofdbijdrage van deze thesis is een aanpak om in toepassingen met een gemeenschappelijke opslagplaats het aantal fouten tijdens de uitvoering sterk te reduceren. We hebben uitgebreid ervaring opgedaan met dergelijke toepassingen in twee toepassingsdomeinen: componentgebaseerde protocolstapels en web toepassingen. Deze ervaringen illustreren duidelijk dat gebroken data afhankelijkheden in dergelijke applicaties een relevant probleem zijn en dat de fouten die eruit voorkomen een belangrijke impact kunnen hebben op de robuustheid en veiligheid van de toepassing. Onze aanpak baseert zich op de formele verificatie van de geen gebroken data afhankelijkheden compositie eigenschap. De formele verificatie van deze eigenschap wordt bereikt in twee stappen.In een eerste stap verifiëren we statisch dat een gegeven compositie met deterministische controle overgangen voldoet aan de gewenste compositie eigenschap. Hiertoe worden de componenten uitgebreid met contracten die de interacties met de gemeenschappelijke opslagplaats beschrijven in een probleemspecifieke contracttaal. Vervolgens volgen twee statische verificatiestappen. Eerst wordt nagegaan of het opgestelde component contract overeenkomt met de implementatie van de component. Ten slotte wordt de compositie eigenschap geverifieerd, steunend op de contracten van de verschillende componenten binnen de compositie.In een tweede stap breiden we de verificatie van de gewenste compositie eigenschap uit naar toepassingen met reactieve controle overgangen. Hierbij wordt de statische verificatie aanpak voor deterministische systemen gecombineerd met verificatie tijdens de uitvoering. Om de statische verificatie mogelijk te maken met de reactieve controle overgangen, definiëren we een bovengrens voor het reactieve gedrag. We noemen dit de vooropgestelde interacties tussen de web gebruiker en de toepassing, en drukken dit protocol uit in een gelabelde toestandsmachine.Daarna verifiëren we statisch of een gegeven compositie voldoet aan de compositie eigenschap, onder de veronderstelling dat elke interactie tussen de web gebruiker en de toepassing deel uitmaakt van de vooropgestelde interactie tussen de web gebruiker en de toepassing. We gebruiken hiervoor de oplossing voorgesteld voor deterministische controle overgangen. Ten slotte gebruiken we de protocolverificatie mogelijkheden van een Web Application Firewall om te garanderen dat enkel web aanvragen die deel uitmaken van de vooropgestelde interactie de web toepassing bereiken. Zo garanderen we dat de geen gebroken data afhankelijkheden compositie eigenschap geldt in een gegeven compositie.Ten slotte hebben we de formele verificatie van de geen gebroken data afhankelijkheden eigenschap gevalideerd in een toepassing met deterministische controle overgangen en een toepassing met reactieve controle overgangen. De statische verificatie uit de eerste stap werd succesvol toegepast op de webmail toepassing GatorMail. GatorMail is een middelgrote, open-source toepassing en bevat in totaal meer dan 1350 interacties met de gemeenschappelijke opslagplaats. Daarnaast werd de combinatie van statische en dynamische verificatie succesvol toegepast op de Duke's Bookstore e-commerce toepassing. In beide validatie experimenten werd een beperkte annotatie- en verificatiekost gemeten. Bovendien illustreerden beide experimenten dat de voorgestelde aanpak lineair schaalt naar grotere, realistische softwaretoepassingen, dankzij de modulaire specificatie en verificatie.
Table of Contents: 1 Introduction
1.1 Background
1.2 Problem Statement
1.3 Main Contributions
1.4 Overview of this Thesis

2 Indirect Data Sharing in Loosely-coupled Component Systems
2.1 Introduction
2.2 Indirect Data Sharing In Data-centered Applications
2.3 Case Study 1: Component-based Web Applications
2.3.1 Web Applications
2.3.2 A Servlet-based E-commerce Application
2.4 Case Study 2: Component-based Protocol Stacks
2.4.1 Protocol Stacks
2.4.2 DiPS+ Rapid Prototyping Infrastructure
2.4.3 A Simplified DiPS+ IPv4 Layer
2.4.4 Development of the DiPS+ Radius Layer
2.5 Goal and Scope of this Work
2.6 Related Work
2.7 Conclusion

3 Dependency Analysis of the GatorMail Webmail Application
3.1 Introduction
3.2 GatorMail
3.2.1 The Struts Framework
3.2.2 Composition Example
3.3 Dependency Analysis
3.3.1 Exploring Dependencies
3.3.2 Heuristic Identification of Dependencies
3.3.3 Abstract Application Model
3.4 Results
3.4.1 Overview of Dependencies
3.4.2 Key Characteristics
3.5 Conclusion

4 Static Verification of Indirect Data Sharing in Loosely-coupled Component Systems
4.1 Introduction
4.2 Background
4.2.1 Component Contracts and Static Verification
4.3 Problem Statement
4.3.1 Simplified Application Model
4.3.2 Composition Example
4.3.3 Desired Composition Properties
4.4 Solution
4.4.1 No Dangling Forwards Property
4.4.2 No Broken Data Dependencies Property
4.4.3 Unsoundness with ESC/Java2
4.5 Validation
4.5.1 Verifying Struts Applications: an Example
4.5.2 Results of the GatorMail Experiment
4.5.3 Discussion
4.6 Related Work
4.7 Conclusion

5 Bridging the Gap Between Web Application Firewalls and Web Applications
5.1 Introduction
5.2 Background
5.2.1 Web Vulnerabilities and Web Application Firewalls (WAFs)
5.3 Problem Statement
5.4 Solution
5.5 Prototype Implementation
5.5.1 Server-side Specification and Verification
5.5.2 Application-specific Protocol Verification
5.5.3 Run-time Protocol Enforcement
5.6 Discussion
5.6.1 Results of the BookStore Experiment
5.6.2 Limitations
5.7 Related Work
5.8 Conclusion

6 Conclusion
6.1 Summary
6.1.1 Main Contributions
6.1.2 Validation
6.2 Future Work
6.3 Developer-centric Verification
6.4 Concluding Thoughts
URI: 
ISBN: 978-90-5682-769-4
Publication status: published
KU Leuven publication type: TH
Appears in Collections:Informatics Section

Files in This Item:
File Description Status SizeFormat
PhD-Desmet-Lieven-final.pdf Published 3791KbAdobe PDFView/Open

 


All items in Lirias are protected by copyright, with all rights reserved.