Abstract
We study a variant of the no read-up/no write-down security property of Bell and LaPadula for processes in the π-calculus. Once processes are given levels of security clearance, we statically check that a process at a high level never sends names to processes at a lower level. The static check is based on a Control Flow Analysis for the π-calculus that establishes a super-set of the set of names to which a given name may be bound and of the set of names that may be sent and received along a given channel, taking into account its directionality. The static check is shown to imply the natural dynamic condition.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
M. Abadi. Secrecy by typing in security protocols. In Proceedings of Theoretical Aspects of Computer Software, Third International Symposioum, LNCS 1281, pages 611–638. Springer-Verlag, 1997.
M. Abadi. Protection in programming-language translations. In Proceedings of ICALP’98, LNCS 1443, pages 868–883. Springer-Verlag, 1998.
R. M. Amadio. An asynchronous model of locality, failure, and process mobility. In Proceedings of COORDINATION’97, LNCS 1282, pages 374–391. Springer-Verlag, 1997.
D. E. Bell and L. J. LaPadula. Secure computer systems: Unified exposition and Multics interpretation. Technical Report ESD-TR-75-306, Mitre C., 1976.
C. Bodei, P. Degano, F. Nielson, and H. Riis Nielson. Control flow analysis for the π-calculus. In Proceedings of CONCUR’98, LNCS 1466, pages 84–98. Springer-Verlag, 1998.
L. Cardelli and A. D. Gordon. Types for mobile ambients. In Proceedings of POPL’99, page (to appear). ACM Press, 1999.
P. Cousot and R. Cousot. Systematic Design of Program Analysis Frameworks. In Proceedings of POPL’ 79, pages 269–282. ACM Press, 1979.
M. Dam. Proving trust in systems of second-order processes: Preliminary results. Technical Report LOMAPS-SICS 19, SICS, Sweden, 1997.
R. De Nicola, G. Ferrari, and R. Pugliese. Coordinating mobile agents via black-boards and access rights. In Proceedings of COORDINATION’97, LNCS 1282, pages 220–237. Springer-Verlag, 1997.
D. E Denning. Cryptography and Data Security. Addison-Wesley, Reading Mass., 1982.
R. Focardi. Comparing two information flow security properties. In Proceedings of 9 th IEEE Computer Science Security Foundation W/S, pages 116–122, 1996.
R. Focardi and R. Gorrieri. The compositional security checker: A tool for the verification of information flow security properties. IEEE Transactions on Software Engineering. To appear.
C. Fournet, C. Laneve, L. Maranget, and D. Remy. Implicit typing à la ML for the join calculus. In Proceedings of CONCUR’97, LNCS 1243, pages 196–212. Springer-Verlag, 1997.
J. A. Goguen and J. Meseguer. Security policy and security models. In Proceedings of the 1982 IEEE Symposioum on Research on Security and Privacy, pages 11–20. IEEE Press, 1982.
N. Heintze and J. G Riecke. The SLam calculus: Programming with secrecy and integrity. In Proceedings of POPL’98, pages 365–377. ACM Press, 1998.
M. Hennessy and J. Riely. Resource access control in systems of mobile agents. Technical Report 2/98, University of Sussex, 1998.
C. E. Landwehr. Formal models for computer security. ACM Computing Surveys, 13(3):247–278, 1981.
T. Lindholm and F. Yellin. The Java Virtual Machine Specification. Addison-Wesley, 1996.
D. McCullough. Specifications for multi-level security and hook-up property. In Proceedings of the 1987 IEEE Symposioum on Research on Security and Privacy. IEEE Press, 1987.
D. McCullough. Noninterference and the composability of security properties. In Proceedings of the 1988 IEEE Symposium on Research on Security and Privacy, pages 177–186. IEEE Press, 1988.
R. Milner, J. Parrow, and D. Walker. A calculus of mobile processes (I and II). Information and Computation, 100(1):1–77, 1992.
R. Milner, J. Parrow, and D. Walker. Modal logics for mobile processes. TCS, 114:149–171, 1993.
G. Necula. Proof-carrying code. In Proceedings of POPL’97, pages 106–119. ACM Press, 1997.
B. C. Pierce and D. Sangiorgi. Typing and sub-typing for mobile processes. Mathematical Structures in Computer Science, 6(5):409–454, 1996.
J. Riely and M. Hennessy. A typed language for distributed mobile processes. In Proceedings of POPL’98, pages 378–390. ACM Press, 1998.
P. Sewell. Global/local subtyping and capability inference for a distributed π-calculus. In Proceedings of ICALP’98, LNCS 1443, pages 695–706. Springer-Verlag, 1998.
A. Venet. Abstract interpretation of the π-calculus. In Analysis and Verification of Multiple-Agent Languages, LNCS 1192, pages 51–75. Springer-Verlag, 1997.
A. Venet. Automatic determination of communication topologies in mobile systems. In Static Analysis Symposium, LNCS 1503, pages 152–167. Springer-Verlag, 1998.
D. Volpano and G. Smith. Secure information flow in a multi-threaded imperative language. In Proceedings of POPL’98, pages 355–364. ACM Press, 1998.
D. Volpano, G. Smith, and C. Irvine. A sound type system for secure flow analysis. Journal of Computer Security, 4:4–21, 1996.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bodei, C., Degano, P., Nielson, F., Nielson, H.R. (1999). Static Analysis of Processes for No Read-Up and No Write-Down. In: Thomas, W. (eds) Foundations of Software Science and Computation Structures. FoSSaCS 1999. Lecture Notes in Computer Science, vol 1578. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-49019-1_9
Download citation
DOI: https://doi.org/10.1007/3-540-49019-1_9
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-65719-4
Online ISBN: 978-3-540-49019-7
eBook Packages: Springer Book Archive