Developing a type inference algorithm for The Ambient Calculus with Kill
Author
Jensen, Casper
Term
4. term
Education
Publication year
2013
Submitted on
2013-06-06
Pages
43
Abstract
This thesis develops a type inference algorithm for the Ambient Calculus with Kill, a formalism for modeling distributed and volunteer computing systems in which nodes may depart. Building on a slightly modified, group-based type system that governs where ambients may reside and whether they can be killed, we present a constraint-driven approach in three stages: (1) generating constraints from a given process P, (2) solving these constraints to obtain a preliminary group environment E and security policy Δ along with group dependencies, and (3) post-processing to resolve dependencies and enforce global typing requirements, yielding final E and Δ. Positioned relative to prior inference work for Mobile Ambients, this contribution explicitly handles the Kill extension. We provide formal correctness results: the E and Δ produced by the algorithm make P well-typed, and the resulting policy Δ is minimal with respect to required permissions.
Denne afhandling udvikler en algoritme til typeinferens for Ambient Calculus med Kill, et formelt rammeværk til at beskrive distribuerede og frivillige beregningssystemer hvor noder kan forlade systemet. Ud fra en let modificeret, gruppebaseret typesystematik, der fastlægger hvor ambienser må befinde sig og om de kan dræbes, præsenterer vi en constraint-baseret tilgang i tre faser: (1) generering af constraints fra en given proces P, (2) løsning af disse constraints for at få et foreløbigt gruppe-miljø E og en sikkerhedspolitik Δ samt gruppeafhængigheder, og (3) efterbehandling der løser afhængighederne og sikrer overordnede typningskrav for at opnå endelige E og Δ. Arbejdet placerer sig i forlængelse af tidligere typeinferens for Mobile Ambients, men adresserer eksplicit Kill-udvidelsen. Vi giver formelle beviser for korrekthed: de E og Δ, som algoritmen returnerer, gør P veltypet, og den afledte politik Δ er minimal i forhold til de nødvendige tilladelser.
[This apstract has been generated with the help of AI directly from the project full text]