The challenges hidden in the implementation of high-level process calculi into low-level environments are well understood. This paper develops a secure implementation of a typed pi calculus, in which capability types are employed to realize the policies for the access to communication channels. Our implementation compiles high-level processes of the pi-calculus into low-level principals of a cryptographic process calculus based on the applied-pi calculus. In this translation, the high-level type capabilities are implemented as term capabilities protected by encryption keys only known to the intended receivers. As such, the implementation is effective even when the compiled, low-level principals are deployed in open contexts for which no assumption on trust and behavior may be made. Our technique and results draw on, and extend, previous work on secure implementation of channel abstractions in a dialect of the join calculus . In particular, our translation preserves the forward secrecy of communications in a calculus that includes matching and supports the dynamic exchange of write and read access-rights among processes. We establish the adequacy and full abstraction of the implementation by contrasting the untyped equivalences of the low-level cryptographic calculus, with the typed equivalences of the high-level source calculus.

Secure implementations of typed channel abstractions

BUGLIESI, Michele;
2007-01-01

Abstract

The challenges hidden in the implementation of high-level process calculi into low-level environments are well understood. This paper develops a secure implementation of a typed pi calculus, in which capability types are employed to realize the policies for the access to communication channels. Our implementation compiles high-level processes of the pi-calculus into low-level principals of a cryptographic process calculus based on the applied-pi calculus. In this translation, the high-level type capabilities are implemented as term capabilities protected by encryption keys only known to the intended receivers. As such, the implementation is effective even when the compiled, low-level principals are deployed in open contexts for which no assumption on trust and behavior may be made. Our technique and results draw on, and extend, previous work on secure implementation of channel abstractions in a dialect of the join calculus . In particular, our translation preserves the forward secrecy of communications in a calculus that includes matching and supports the dynamic exchange of write and read access-rights among processes. We establish the adequacy and full abstraction of the implementation by contrasting the untyped equivalences of the low-level cryptographic calculus, with the typed equivalences of the high-level source calculus.
2007
Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2007
File in questo prodotto:
File Dimensione Formato  
p251-bugliesi.pdf

non disponibili

Tipologia: Documento in Post-print
Licenza: Accesso chiuso-personale
Dimensione 275.26 kB
Formato Adobe PDF
275.26 kB Adobe PDF   Visualizza/Apri

I documenti in ARCA sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/10278/30693
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? 17
social impact