×

A model checking-based approach for security policy verification of mobile systems. (English) Zbl 1242.68153


MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
PDFBibTeX XMLCite
Full Text: DOI HAL

References:

[1] Bellavista P, Corradi A (2006) The handbook of mobile middleware. Auerbach Publications, Boston
[2] Beyer D, Chlipala AJ, Henzinger TA, Jhala R, Majumdar R (2004) The BLAST query language for software verification. In: LNCS. Springer, New York, pp 2–18 · Zbl 1104.68408
[3] Ball T, Cook B, Levin V, Rajamani SK (2004) Slam and static driver verifier: technology transfer of formal methods inside microsoft. In: Boiten EA, Derrick J, Smith G (eds) IFM, Lecture notes in computer science, vol 2999. Springer, New York, pp. 1–20
[4] Bell DE, La Padula LJ (1976) Secure computer systems: unified exposition and multics interpretation. ESD-TR-75-306, MITRE MTR-2997, MITRE Corporation, March 1976
[5] Bettini L, De Nicola R, Loreti M (2002) Software update via mobile agent based programming. In: SAC. ACM, pp 32–36
[6] Ball T, Rajamani SK (2000) Bebop: a symbolic model checker for Boolean Programs. In: SPIN 00: SPIN workshop. LNCS 1885. Springer-Verlag, pp 113–130 · Zbl 0976.68540
[7] Ball T, Rajamani SK (2001) The slam toolkit. In: Berry G, Comon H, Finkel A (eds) CAV. Lecture notes in computer science, vol 2102. Springer, New York, pp 260–264 · Zbl 0996.68560
[8] Ball T, Rajamani SK (2002) SLIC: a specification language for interface checking (of C). Technical report MSR-TR-2001-21, Microsoft Research
[9] Burkart O, Steffen B (1995) Composition, decomposition and model checking of pushdown processes. Nord J Comput 2: 89–125 · Zbl 0839.68028
[10] Bidinger P, Stefani JB (2003) The Kell calculus: operational semantics and type system. In: Formal methods for open object-based distributed systems, 6th IFIP WG 6.1 international conference, FMOODS 2003, Paris, France, 2005, Proceedings. Lecture notes in computer science, vol 2884. Springer, New York · Zbl 1253.68235
[11] Braghin C, Sharygina N, Barone-Adesi K (2007) Automated verification of security policies in mobile code. In: Integrated formal methods (IFM07), LNCS, vol 4591, pp 37–53 · Zbl 1242.68153
[12] Bidinger P, Schmitt A, Stefani J-B (2005) An abstract machine for the Kell calculus. In: Formal methods for open object-based distributed systems, 7th IFIP WG 6.1 international conference, FMOODS 2005, Athens, Greece, 2005, Proceedings. Lecture notes in computer science, vol 3535, pp 43–58
[13] Cerný P, Alur R (2009) Automated analysis of Java methods for confidentiality. In: Computer aided verification (CAV09), pp 173–187
[14] Cardelli L (1999) Wide area computation. In: Wiedermann J, van Emde Boas P, Nielsen M (eds) Proceedings of 26th international colloquium in automata, languages and programming (ICALP’99). Lecture notes in computer science, vol 1644. Springer-Verlag, Berlin, pp 10–24 (Invited Paper)
[15] Chaki S, Clarke EM, Kidd N, Reps TW, Touili T (2006) Verifying concurrent message-passing C programs with recursive calls. In: Hermanns H, Palsberg J (eds) Proceedings of the 12th international conference on tools and algorithms for the construction and analysis of systems (TACAS). Lecture notes in computer science, vol 3920. Springer, New York, pp 334–349 · Zbl 1180.68109
[16] Chaki S, Clarke E, Ouaknine J, Sharygina N, Sinha N (2004) State/event-based software model checking. In: IFM 2004, pp 128–147 · Zbl 1196.68129
[17] Charatonik W, Zilio SD, Gordon AD, Mukhopadhyay S, Talbot J-M (2002) Finite-control mobile ambients. In: Proceedings of European symposium on programming (ESOP02). Lecture notes in computer science, vol 2305. Springer-Verlag, Berlin, pp 295–313 · Zbl 1077.68574
[18] Cardelli L, Gordon AD (2000) Mobile ambients. Theor Comput Sci 240(1): 177–213 · Zbl 0954.68108 · doi:10.1016/S0304-3975(99)00231-5
[19] Chaki S, Ivers J, Sharygina N, Wallnau KC (2005) The comfort reasoning framework. In: Etessami K, Rajamani SK (eds) CAV. Lecture notes in computer science, vol 3576. Springer, New York, pp 164–169 · Zbl 1081.68613
[20] Cook B, Kroening D, Sharygina N (2005) Symbolic model checking for asynchronous boolean programs. In: Proceedings of SPIN. Springer-Verlag, New York, pp 75–90 · Zbl 1151.68367
[21] Cook B, Kroening D, Sharygina N (2006) Over-approximating Boolean programs with unbounded thread creation. In FMCAD 06: formal methods in system design. Springer-Verlag, New York · Zbl 1143.68043
[22] Clarke E, Kroening D, Sharygina N, Yorav K (2005) SATABS: SAT-based predicate abstraction for ANSI-C. In: TACAS. LNCS, vol 3440. Springer-Verlag, New York, pp 570–574 · Zbl 1087.68586
[23] IBM Corporation (1999) Aglet software development kit
[24] Clarke E, Talupur M, Touili T, Veith H (2004) Verification by network decomposition. In: CONCUR 04. Springer-Verlag, New York, pp 276–291 · Zbl 1099.68653
[25] Distefano D (2000) A parametric model for the analysis of mobile ambients. In: 3rd Asian symposium on programming languages and systems (APLAS 2005). Tsukuba, Japan. LNCS 3780, pp 401–417. Springer 2005, pp 305–326. Kluwer Academic Publishers · Zbl 1159.68367
[26] De Nicola R, Ferrari G, Pugliese R (1998) Klaim: a Kernel language for agents interaction and mobility. IEEE Trans Softw Eng 24(5): 315–330 · doi:10.1109/32.685256
[27] US Department of Defence (1985) DoD trusted system evaluation criteria (The Orange Book), vol DOD 5200.28-STD. June 1985
[28] Esparza J, Schwoon S (2001) A BDD-based model checker for recursive programs. In: CAV, LNCS 2102. Springer-Verlag, New York, pp 324–336 · Zbl 0991.68539
[29] Fournet C, Gonthier G, Lévy J-J, Maranget L, Rémy D (1996) A calculus of mobile agents. In: Proceedings of the 7th international conference on concurrency theory (CONCUR’96). Springer-Verlag, Berlin, pp 406–421
[30] Flanagan C, Qadeer S (2003) Thread-modular model checking. In: Proceedings of the 10th international workshop on model checking software (SPIN). Lecture notes in computer science, vol 2648. Springer, New York, pp 213–224 · Zbl 1023.68529
[31] Henzinger TA, Jhala R, Majumdar R (2004) Race checking by context inference. In: Pugh W, Chambers C (eds) Proceedings of the ACM SIGPLAN 2004 conference on programming language design and implementation (PLDI). ACM, pp 1–13
[32] Havelund K, Pressburger T (2000) Model checking Java programs using Java PathFinder. Int J Softw Tools Technol Transfer 2(4) · Zbl 1059.68585
[33] Hennessy M, Riely J (1998) Resource access control in systems of mobile agents. In: HLCL ’98, J TCS. Elsevier, pp 3–17 · Zbl 0917.68047
[34] Ip CN, Dill DL (1996) Verifying systems with replicated components in Mur{\(\Phi\)}. In: Proceedings of CAV, vol 1102. Springer-Verlag, pp 147–158
[35] Kurshan R (1995) Computer-aided verification of coordinating processes. Princeton University Press, Princeton · Zbl 0822.68116
[36] McLean J (1994) Security models. In: Marciniak J (ed) Encyclopedia of software engineering. Wiley
[37] Sum Microsystems (1995) The Java language specification
[38] MOBIUS (Mobility, Ubiquity and Security) European Project. http://mobius.inria.fr
[39] Necula GC, Lee P (1997) Research on proof-carrying code for untrusted-code security. In: IEEE symposium on security and privacy, p 204
[40] Pnueli A, Arons T (2003) TLPVS: a PVS-based LTL verification system. In: Verification-theory and practice: proceedings of an international symposium in honor of Zohar Manna’s 64th birthday. Lecture notes in computer science. Springer-Verlag, New York, pp 84–98
[41] Rinard M (2001) Analysis of multithreaded programs. Lecture notes in computer science, vol 2126 · Zbl 1005.68896
[42] Roscoe AW (1998) The theory and practice of concurrency. Prentice-Hall
[43] S3MS (Security of Software and Services for Mobile Systems) European Project. http://www.s3ms.org
[44] Schneider FB (2000) Enforceable security policies. ACM Trans Inf Syst Secur 3(1). February 2000
[45] Schmitt A, Stefani JB (2004) The Kell calculus: a family of higher-order distributed process calculi. In: Global computing. Lecture notes in computer science. Springer
[46] Stefani JB (2003) A calculus of Kells. ENTCS 85(1) · Zbl 1270.68226
[47] Stoller S (2000) Model-checking multi-threaded distributed Java programs. In: SPIN 00: international SPIN workshop on SPIN model checking and software verification. Springer-Verlag · Zbl 0976.68556
[48] Sharygina N, Tonetta S, Tsitovich A (2009) The synergy of precise and fast abstractions for program verification. In: Shin SY, Ossowski S (eds) SAC. ACM, pp 566–573
[49] White JE (1994) Telescript technology: the foundation of the electronic marketplace. Technical report, General Magic Inc
[50] Yahav E (2001) Verifying safety properties of concurrent Java programs using 3-valued logic. In: POPL, pp 27–40 · Zbl 1323.68183
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.