The secret pi calculus is a variant of the pi calculus that features both dynamic and static communication channels; differently from dynamic channels, the scope of static channels cannot be extruded. This is achieved during the execution by means of a mechanism of accepted/blocked channels in process rearrangement; the construction can be interpreted as a monitored run-time system. In this talk, we present a type system for a standard pi calculus that allows to represent the secret channel abstractions through static and dynamic type modalities for channels (scope). The main aim is to provide a abstract API for secure message-passing communication : the programmer declares which channels are meant to be secret, the compiler enforces a static scope by means of static type-checking. Towards this direction, we discuss ongoing work on type inference of static and dynamic types, and attack some examples with the ocaml/z3 implementation.
Short Bio: Marco Giunti obtained his PhD from Venice University, Italy, and subsequently held post-doc positions at the University of Lisbon, Ecole Polytechnique Palaiseau, NOVA University of Lisbon, and University of Porto. Before joining FCUL as invited professor he was an invited professor at the University of Beira Interior, in the RELiablE And SEcure Computation Group. Marco's main interests focus on the formal aspects of message-passing concurrent programs, ranging from semantic theories for program equivalence, to program correctness and security through type systems and program logics, and program enhancement through program transformation techniques.
