'Type Checking Versus Flow Logics'
Authors
Jensen, Lars Hornbæk ; Vester, Bjørn Mølgård
Term
4. term
Education
Publication year
2006
Abstract
Dette projekt undersøger, hvordan kontrolflowanalyse (at kortlægge de mulige forløb et program eller en proces kan have) hænger sammen med typekontrol (at sikre, at værdier og operationer bruges konsistent). Vi udvikler en typet version af LySa-kalkylen, der bruger korrespondenspåstande, samt et tilhørende typesystem. Vi konstruerer en kodning fra processer med kryptopunkter i LySa til Typed LySa og viser, at de har ækvivalente sikkerhedsegenskaber. Typeudledning udføres på den kodede proces under en række begrænsninger. Til sidst skaber vi en ny kontrolflowanalyse, der bruger korrespondenspåstande i stedet for kryptopunkter.
This project explores how control flow analysis (studying the possible paths a program or process can take) relates to type checking (ensuring values and operations are used consistently). We create a typed version of the LySa calculus that uses correspondence assertions, along with a matching type system. We construct an encoding from LySa processes with crypto-points to Typed LySa and show that they have equivalent safety properties. Type inference is performed on the encoded process under a series of constraints. Finally, we design a new control flow analysis that uses correspondence assertions instead of crypto-points.
[This abstract was generated with the help of AI]
Documents