Hybrid logical analyses of the ambient calculus
Pages 433 - 449
Abstract
In this paper, hybrid logic is used to formulate three control flow analyses for Mobile Ambients, a process calculus designed for modelling mobility. We show that hybrid logic is very well-suited to express the semantic structure of the ambient calculus and how features of hybrid logic can be exploited to reduce the ''administrative overhead'' of the analysis specification and thus simplify it. Finally, we use HyLoTab, a fully automated theorem prover for hybrid logic, both as a convenient platform for a prototype implementation as well as to formally prove the correctness of the analysis.
References
[1]
Cardelli, L. and Gordon, A.D., Mobile ambients. Theoretical Computer Science. v240. 177-213.
[2]
Nielson, H.R. and Nielson, F., Flow logic: a multi-paradigmatic approach to static analysis. In: Lecture Notes in Computer Science, vol. 2566. Springer-Verlag. pp. 223-244.
[3]
Nielson, F., Hansen, R.R. and Nielson, H.R., Abstract interpretation of mobile ambients. Science of Computer Programming. v47 i2--3. 145-175.
[4]
J. van Eijck, Constraint Tableaux for Hybrid Logics, Manuscript, CWI, Amsterdam, 2002.
[5]
Nielson, F., Nielson, H.R. and Hansen, R.R., Validating firewalls using flow logics. Theoretical Computer Science. v283 i2. 381-418.
[6]
H.R. Nielson, F. Nielson, Shape analysis for mobile ambients, in: Conference Record of the Annual ACM Symposium on Principles of Programming Languages, POPL'00, ACM Press, 2000, pp. 142--154.
[7]
T. Bolander, R.R. Hansen, Hybrid logical analyses of the ambient calculus, in: D. Leivant, R. de Queiroz (Eds.), Workshop on Logic, Language, Information and Computation (WoLLIC'07), Lecture Notes in Computer Science, vol. 4576, Springer-Verlag, Rio de Janeiro, Brazil, 2007, pp. 83--100.
[8]
Nielson, H.R., Nielson, F. and Buchholtz, M., Security for mobility. In: Focardi, R., Gorrieri, R. (Eds.), Lecture Notes in Computer Science, vol. 2946. Springer. pp. 207-265.
[9]
R.R. Hansen, J.G. Jensen, Flow logics for mobile ambients, Master's Thesis, Aarhus University, 1999.
[10]
Hansen, R.R., Jensen, J.G., Nielson, F. and Nielson, H.R., Abstract interpretation of mobile ambients. In: Cortesi, A., Filé, G. (Eds.), Lecture Notes in Computer Science, vol. 1694. Springer-Verlag, Venice, Italy. pp. 134-148.
[11]
F. Nielson, H.R. Nielson, R.R. Hansen, J.G. Jensen, Validating firewalls in mobile ambients, in: International Conference on Concurrency Theory (CONCUR'99), 1999, pp. 463--477Available from: <citeseer.ist.psu.edu/nielson99validating.html>.
[12]
Blackburn, P., de Rijke, M. and Venema, Y., Modal logic. In: Cambridge Tracts in Theoretical Computer Science, vol. 53. Cambridge University Press, Cambridge, UK.
[13]
T. Braüner, Natural deduction for hybrid logic, Journal of Logic and Computation 14 (3) (2004) 329--353. Available from: <http://dx.doi.org/10.1093/logcom/14.3.329>.
[14]
Cardelli, L. and Gordon, A.D., Anytime, anywhere: modal logics for mobile ambients. In: Conference Record of the Annual ACM Symposium on Principles of Programming Languages, POPL'00, ACM Press. pp. 365-377.
[15]
J. van Eijck, HyLoTab---Tableau-based Theorem Proving for Hybrid Logics, Manuscript, CWI, Amsterdam, 2002.
[16]
C. Braghin, Static analysis of security properties in Mobile Ambients, Ph.D. Thesis, Università Ca' Foscari di Venezia, TD-2005-1, 2005. Available from: <http://www.unive.it/media/dipInformatica/phd/CBraghin_thesis_hyperlinks3.pdf.>.
[17]
ten Cate, B. and Franceschet, M., On the complexity of hybrid logics with binders. In: Lecture Notes in Computer Science, vol. 3634. Springer-Verlag. pp. 339-354.
[18]
T. Bolander, P. Blackburn, Terminating tableau calculi for hybrid logics extending K, in: Proceedings of Methods for Modalities 5 (M4M-5), 2007.
[19]
Cardelli, L. and Gordon, A.D., Types for mobile ambients. In: Conference Record of the Annual ACM Symposium on Principles of Programming Languages, POPL'99, ACM Press. pp. 79-92.
[20]
T. Amtoft, H. Makholm, J.B. Wells, Polya: true type polymorphism for mobile ambients, in: J.-J. Levy, E.W. Mayr, J.C. Mitchell (Eds.), TCS 2004 (Third IFIP International Conference on Theoretical Computer Science), Toulouse, France, August 2004, Kluwer Academic Publishers, 2004, pp. 591--604.
[21]
Amtoft, T., Kfoury, A.J. and Pericas-Geertsen, S.M., What are polymorphically-typed ambients?. In: Sands, D. (Ed.), LNCS, vol. 2028. Springer-Verlag. pp. 206-220.
[22]
C. Calcagno, P. Gardner, U. Zarfaty, Context logic and tree update, in: Conference Record of the Annual ACM Symposium on Principles of Programming Languages, POPL'05, ACM, 2005, pp. 271--282.
- Hybrid logical analyses of the ambient calculus
Recommendations
Hybrid logical analyses of the ambient calculus
WoLLIC'07: Proceedings of the 14th international conference on Logic, language, information and computationIn this paper, hybrid logic is used to formulate a rational reconstruction of a previously published control flow analysis for the mobile ambients calculus and we further show how a more precise flow-sensitive analysis, that takes the ordering of action ...
Axioms for classical, intuitionistic, and paraconsistent hybrid logic
In this paper we give axiom systems for classical and intuitionistic hybrid logic. Our axiom systems can be extended with additional rules corresponding to conditions on the accessibility relation expressed by so-called geometric theories. In the ...
Decidability of a Hybrid Duration Calculus
We present a logic which we call Hybrid Duration Calculus (HDC). HDC is obtained by adding the following hybrid logical machinery to the Restricted Duration Calculus (RDC): nominals, satisfaction operators, down-arrow binder, and the global modality. ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
Copyright © Elsevier Inc. © 2009.
Publisher
Academic Press, Inc.
United States
Publication History
Published: 01 May 2010
Author Tags
Qualifiers
- Article
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 0Total Downloads
- Downloads (Last 12 months)0
- Downloads (Last 6 weeks)0
Reflects downloads up to 14 Dec 2024