Kohei Honda
ABSTRACT
The π-calculus is a formalism of computing in which we can compositionally represent dynamics of major programming constructs by decomposing them into a single communication primitive, the name passing. This work reports our experience in using a linear/affine typed π-calculus for the analysis and development of type systems of programming languages, focussing on secure information flow analysis. After presenting a basic typed calculus for secrecy, we demonstrate its usage by a sound embedding of the dependency core calculus (DCC) and by the development of a novel type discipline for imperative programs which extends both a secure multi-threaded imperative language by Smith and Volpano and (a call-by-value version of) DCC. In each case, the embedding gives a simple proof of noninterference.
- 1.Abadi, M., Secrecy in programming-language semantics, MFPS XV, ENTCS, 20 (April 1999).]]Google Scholar
- 2.Abadi, M., Banerjee, A., Heintze, N. and Riecke, J., A core calculus of dependency, POPL'99, ACM, 1999.]] Google ScholarDigital Library
- 3.Abramsky, S., Jagadeesan, R. and Malacaria, P., Full Abstraction for PCF, 1994. Info. Comp. 163 (2000), 409-470.]] Google ScholarDigital Library
- 4.Abramsky, S., Honda, K. and McCusker, G., Fully Abstract Game Semantics %r General Re%rences, LICS'98, 334-344, IEEE, 1998.]] Google ScholarDigital Library
- 5.Agat, J. Transforming Out Timing Leaks, POPL'O0, 2000, ACM Press.]] Google ScholarDigital Library
- 6.Berger, M., Honda, K. and Yoshida, N., Sequentiality and tile -Calculus, TLCA01, LNCS 2044, 29-45, Springer, 2001.]]Google Scholar
- 7.Boudol, G., Asynchrony and the pi-calculus, INRIA Research Report 1702, 1992.]]Google Scholar
- 8.Boudol, G. and Castellani, I., Noninterference for Concurrent Programs, ICALPO1, LNCS 2076, 382-395, Springer, 2001.]] Google ScholarDigital Library
- 9.Denning, D. and Denning, P., Certification of programs for secure information flow. Communication of ACM, ACM, 20:504-513, 1997.]] Google ScholarDigital Library
- 10.Focardi, R., Gorrieri, R. and Martinelli, F., Non-inter%rence for the analysis of cryptographic protocols. ICALPO0, LNCS 1853, Springer, 2000.]] Google ScholarDigital Library
- 11.Girard, J.-Y., Linear Logic, TCS, Vol. 50, 1-102, 1987.]] Google ScholarDigital Library
- 12.Heintze, N. and Riecke, J., The SLam calculus: programming with secrecy and integrity, POPL'98, 365-377, ACM, 1998.]] Google ScholarDigital Library
- 13.Hennessy, M. and Riely, J., Information flow as resource access in the asynchronous pi-calculus, ICALPO0, LNCS 1853, 415-427, Springer, 2000.]] Google ScholarDigital Library
- 14.Honda, K., Types for Dyadic Interaction. CONCUR'93, LNCS 715, 509-523, 1993.]] Google ScholarDigital Library
- 15.Honda, K., Composing Processes, POPL'96, 344-357, ACM, 1996.]] Google ScholarDigital Library
- 16.Honda, K., Kubo, M. and Vasconcelos, V., Language Primitives and Type Discipline for Structured Communication-Based Programming. ESOP'98, LNCS 1381, 122 138. Springer-Verlag, 1998.]] Google ScholarDigital Library
- 17.Honda, K. and Tokoro, M. An object calculus asynchronous communication. ECOOP'91, LNCS 512, 133-147, 1991.]] Google ScholarDigital Library
- 18.Honda, K., Vasconcelos, V. and Yoshida, N., Secure Information Flow as Typed Process Behaviour, ESOP'O0, LNCS 1782, 180 199, 2000.]] Google ScholarDigital Library
- 19.Honda, K. and Yoshida, N. On Reduction-Based Process Semantics. TCS. 151,437-486, 1995.]] Google ScholarDigital Library
- 20.Honda, K. and Yoshida, N. Game-theoretic analysis of call-by-value computation. TCS, 221 (1999), 393 456.]] Google ScholarDigital Library
- 21.Howard, B. T., Inductive, coinductive, and pointed types, ICFP'96, 102 109, ACM, 1996.]] Google ScholarDigital Library
- 22.The Haskell home page, http://haskell.org.]]Google Scholar
- 23.Hyland, M. and Ong, L., "On Full Abstraction for PCF": I, II and III. Info. Comp. 163 (2000), 285-408.]] Google ScholarDigital Library
- 24.Kobayashi, N., Pierce, B., and Turner, D., Linear types and re-calculus, POPL'96, 358-371, 1996.]] Google ScholarDigital Library
- 25.Milner, R., Functions as Processes, MSCS. 2(2):119 141, 1992,]]Google Scholar
- 26.Milner, R., Parrow, J. and Walker, D., A Calculus of Mobile Processes, Info. f3 Cornp. 100(1):1-77, 1992.]] Google ScholarDigital Library
- 27.Mitchell, J., Foundations for Programming Languages MIT Press, 1996.]] Google ScholarDigital Library
- 28.Palsberg, J. and 2~rbaek , J., Trust in the A-Calculus. JFP, 7(6):557-591, 1997.]] Google ScholarDigital Library
- 29.Potter, F. and Conchon, S, Information flow inference for free, ICFPO0, 46-57, ACM, 2000.]] Google ScholarDigital Library
- 30.Pierce, B and Sangiorgi.D, Typing and subtyping for mobile processes, MSCS 6(5):409-453, 1996.]]Google Scholar
- 31.Ryan, P. and Schneider, S. Process Algebra and Non-interference. CSFW'99, IEEE, 1999.]] Google ScholarDigital Library
- 32.Sangiorgi, D. re-calculus, internal mobility, and agent-passing calculi. TCS, 167(2):235-271, 1996.]] Google ScholarDigital Library
- 33.Sabelfield, A. and Sand, D. A per model of secure information flow in sequential programs. ESOP'99, LNCS 1576, Springer, 1999.]] Google ScholarDigital Library
- 34.Smith, G., A New Type System for Secure Information Flow, CSFW'01, IEEE, 2001.]] Google ScholarDigital Library
- 35.Smith, G. and Volpano, D., Secure information flow in a multi-threaded imperative language, 355-364, POPL'98, ACM, 1998.]] Google ScholarDigital Library
- 36.ToKe, M., Type in%rence tbr polymorphic references, Info. f3 Conp., 89:1-34, 1990.]] Google ScholarDigital Library
- 37.Vasconcelos, V., Typed concurrent objects. ECOOP'9d, LNCS 821, 100-117. Springer, 1994.]] Google ScholarDigital Library
- 38.Volpano, D., Smith, G. and Irvine, C., A Sound type system for secure, flow analysis, a. Computer Security, 4(2,3):167-187, 1996.]] Google ScholarDigital Library
- 39.Yoshida, N. Graph Types for Mobile Processes. FST/TCS'16, LNCS 1180, 371-386, Springer, 1996.]] Google ScholarDigital Library
- 40.Yoshida, N., Berger, M. and Honda, K., Strong Normalisation in the re-Calculus, LICS'01, 311-322, (C1) (C2) (C3) IEEE, 2001.]]Google ScholarCross Ref
- 41.Yoshida, N., Honda, K. and Berger, M., Linearity and Bisimulation, To appear as MCS technical report, Leicester, 2001.]]Google Scholar
- 42.Zdancewic, S. and Myers, A., Secure Information Flow and CPS, ESOP01, LNCS 2028, 46-62, Springer, 2001.]] Google ScholarDigital Library
- A uniform type structure for secure information flow
Recommendations
A uniform type structure for secure information flow
The π-calculus, a calculus of mobile processes, can compositionally represent dynamics of major programming constructs by decomposing them into name passing. The present work reports our experience in using a linear/affine typed π-calculus for the ...
A uniform type structure for secure information flow
The π-calculus is a formalism of computing in which we can compositionally represent dynamics of major programming constructs by decomposing them into a single communication primitive, the name passing. This work reports our experience in using a linear/...
A Haskell-Embedded DSL for Secure Information-Flow
Formal Methods: Foundations and ApplicationsAbstractThis paper presents a domain specific language, embedded in Haskell (EDSL), for enforcing the information flow policy Delimited Release. To build this language we use Haskell extensions that will allow some kind of dependently-typed programming.
...
Comments