Formally Defining Document Object Model Cross-site Scripting Exploits using Propositional Dynamic Logic
Cross-site scripting behoort tot de meest voorkomende kwetsbaarheden in webbeveiliging, maar naar de meest complexe variant — Document Object Model XSS — is formeel nog weinig onderzoek gedaan. In deze scriptie presenteer ik een formeel raamwerk waarin DOM XSS-exploits worden gedefinieerd in propositionele dynamische logica, benaderdt vanuit het perspectief van de aanvaller. Het model maakt het mogelijk te redeneren over de voorwaarden waaronder exploitatie mogelijk is.
Aanleiding
DOM XSS onderscheidt zich van reflected XSS en stored XSS doordat de payload de server niet hoeft te passeren: de kwetsbaarheid ontstaat volledig binnen de browser, wanneer vanuit de aanvaller invoer via JavaScript in de Document Object Model terechtkomt. Juist doordat het probleem structureel van aard is, is het moeilijk om effectieve preventiemaatregelen te gebruiken.
In de praktijk wordt veelal gewerkt met blacklisting en whitelisting aan de hand van scanners die op gevoelige strings filteren. Echter, DOM XSS wordt verricht aan de hand van een proces. Aan de hand van propositionele dynamische logica kunnen exploits specifiek worden uitgedrukt. Hierbij dien ik uiterst nauwkeurig te beschrijven hoe DOM XSS-exploits in een logica-raamwerk kunnen worden uitgedrukt. Dat zou later de basis kunnen vormen voor het opstellen van specifiekere preventiemaatregelen tegen dergelijke exploits.
Het model
Het raamwerk is gebouwd op een gecombineerd toestandsmodel dat twee componenten samenbrengt. Pas wanneer beide in één toestand worden beschreven, kan worden vastgesteld of een payload daadwerkelijk tot uitvoering komt.
De DOM als toestandsruimte
De structurele eigenschappen van het document worden weergegeven als een grove van uniek te-identificeren nodes, zodat over de plaats van een node binnen het document geredeneerd kan worden.
De JavaScript-omgeving
Een variabelenomgeving die bijhoudt hoe payload van de aanvaller gedurende de uitvoering van het script worden getransformeerd.
Programmatransities zijn ondergebracht in drie semantische klassen, die samen beschrijven hoe een payload van de aanvaller, via tussenliggende transities, uiteindelijk de DOM verandert.
- Source — de plek waar de payload van de aanvaller de omgeving binnenkomt.
- Flow — de transformaties die de payload ondergaat: toewijzing, concatenatie, encoding, decoding en sanitisatie. Die laatste maakt het mogelijk te redeneren over bypass-technieken.
- Sink — de plek waar de payload in de documentstructuur belandt en tot uitvoering kan komen.
Een exploittoestand is vervolgens gedefinieerd als een toestand die de kwaadaardige payload tot een sink brengt. Daarmee is nauwkeurig vastgelegd wanneer de exploit van een aanvaller is geslaagd.
Validatie
De geldigheid van de formalisatie is aangetoond aan de hand van drie voorbeelden, waarvan het laatste bewust de grens van het model opzoekt.
Een verkeerd toegepaste sanitizer
Het eerste voorbeeld toont een exploit die mogelijk blijft ondanks de aanwezigheid van een sanitizer, omdat deze sanitizer op de verkeerde variabele wordt toegepast.
Bypass via dubbele decodering
Het tweede voorbeeld laat een bypass zien waarbij tweemaal wordt gedecodeerd, doordat de payload zelf ook dubbel geëncodeerd kan zijn.
De grenzen van de formalisatie
Het derde voorbeeld toont aan dat een DOM clobbering-aanval niet door het formele model kan worden gevangen, en maakt daarmee de beperkingen van de formalisatie expliciet.
Opbouw van het rapport
- 1Introduction
- 2Related Work
- 3Background — cross-site scripting en logica
- 4Conceptualizing DOM XSS
- 5Formalization in Propositional Dynamic Logic
- 6Validation — drie uitgewerkte voorbeelden
- 7Discussion
- 8Conclusion
De volledige scriptie
Mijn volledige Master Thesis, inclusief de formele definities, de transitieregels en de uitgewerkte voorbeelden.