Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Published in:
Secure Two-Party Computation in Applied Pi-Calculus: Models and Verification Read chapter Read first chapter

2016 | OriginalPaper | Chapter

Data Tracking in Parameterized Systems

Author : Giorgio Delzanno

Published in: Trustworthy Global Computing

Publisher: Springer International Publishing

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

We study parameterized verification problems for concurrent systems with data enriched with a permission model for invoking remote services. Processes are modelled via register automata. Communication is achieved by rendez-vous with value passing. Permissions are represented as graphs with an additional conflict relation to specify incompatible access rights. The resulting model is inspired by communication architectures underlying operating systems for mobile devices. We consider decision problems involving permission violations and data tracking formulated for an arbitrary number of processes and use reductions to well structured transition systems to obtain decidable fragments of the model.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

inform now
previous chapter Multiparty Testing Preorders
next chapter Modular Monitor Extensions for Information Flow Security in JavaScript
Literature
1.
Abdulla, P.A., Delzanno, G., Van Begin, L.: A classification of the expressive power of well-structured transition systems. Inf. Comput. 209(3), 248–279 (2011)CrossRefMathSciNetMATH
2.
Armando, A., Costa, G., Merlo, A.: Formal modeling and reasoning about the android security framework. In: Palamidessi, C., Ryan, M.D. (eds.) TGC 2012. LNCS, vol. 8191, pp. 64–81. Springer, Heidelberg (2013)CrossRef
3.
Armando, A., Ranise, S.: Scalable automated symbolic analysis of administrative role-based access control policies by SMT solving. J. Comput. Secur. 20(4), 309–352 (2012)
4.
Arons, T., Pnueli, A., Ruah, S., Xu, J., Zuck, L.D.: Parameterized verification with automatically computed inductive assertions. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 221–234. Springer, Heidelberg (2001)CrossRef
5.
Bartoletti, M., Degano, P., Ferrari, G.-L., Zunino, R.: Types and effects for resource usage analysis. In: Seidl, H. (ed.) FOSSACS 2007. LNCS, vol. 4423, pp. 32–47. Springer, Heidelberg (2007)CrossRef
6.
Bartoletti, M., Degano, P., Ferrari, G.L., Zunino, R.: Local policies for resource usage analysis. ACM TOPLAS, vol. 31(6) (2009)
7.
Bartoletti, M., Degano, P., Ferrari, G.L., Zunino, R.: Model checking usage policies. MSCS 25(3), 710–763 (2015)MathSciNet
8.
Bozzano, M.: A Logic-Based Approach to Model Checking of Parameterized and Infinite-State Systems, Ph.D. thesis, DISI, University of Genova, June 2002
9.
Bugliesi, M., Calzavara, S., Spanò, A.: Lintent: towards security type-checking of android applications. In: Beyer, D., Boreale, M. (eds.) FORTE 2013 and FMOODS 2013. LNCS, vol. 7892, pp. 289–304. Springer, Heidelberg (2013)CrossRef
10.
Delzanno, G.: An overview of MSR(C): A CLP-based framework for the symbolic verification of parameterized concurrent systems. ENTCS 76, 65–82 (2002)
11.
Delzanno, G.: Constraint-based automatic verification of abstract models of multithreaded programs. TPLP 7(1–2), 67–91 (2007)MathSciNetMATH
12.
Delzanno, G., Rosa-Velardo, F.: On the coverability and reachability languages of monotonic extensions of petri nets. Theor. Comput. Sci. 467, 12–29 (2013)CrossRefMathSciNetMATH
13.
Delzanno, G., Sangnier, A., Traverso, R., Zavattaro, G.: On the complexity of parameterized reachability in reconfigurable broadcast networks. In: FSTTCS 2012, pp. 289–300 (2012)
14.
Delzanno, G., Sangnier, A., Zavattaro, G.: Parameterized verification of ad hoc networks. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010. LNCS, vol. 6269, pp. 313–327. Springer, Heidelberg (2010)CrossRef
15.
Delzanno, G., Sangnier, A., Zavattaro, G.: On the Power of Cliques in the Parameterized Verification of Ad Hoc Networks. In: Hofmann, M. (ed.) FOSSACS 2011. LNCS, vol. 6604, pp. 441–455. Springer, Heidelberg (2011)CrossRef
16.
Emerson, E.A., Namjoshi, K.S.: On model checking for non-deterministic infinite-state systems. In: LICS, pp. 70–80 (1998)
17.
Esparza, J., Finkel, A., Mayr, R.: On the verification of broadcast protocols. In: LICS 1999, pp. 352–359 (1999)
18.
19.
Lazic, R., Newcomb, T., Ouaknine, J., Roscoe, A.W., Worrell, J.: Nets with tokens which carry data. Fundam. Inform. 88(3), 251–274 (2008)MathSciNetMATH
20.
Majumdar, R., Meyer, R., Wang, Z.: Provenance verification. In: RP, pp. 21–22 (2013)
21.
Ranise, S.: Symbolic backward reachability with effectively propositional logic - applications to security policy analysis. FMSD 42(1), 24–45 (2013)MATH
22.
Ranise, S., Traverso, R.: ALPS: an action language for policy specification and automated safety analysis. In: Mauw, S., Jensen, C.D. (eds.) STM 2014. LNCS, vol. 8743, pp. 146–161. Springer, Heidelberg (2014)
23.
Rosa-Velardo, F., de Frutos-Escrig, D.: Decidability results for restricted models of petri nets with name creation and replication. In: Franceschinis, G., Wolf, K. (eds.) PETRI NETS 2009. LNCS, vol. 5606, pp. 63–82. Springer, Heidelberg (2009)CrossRef
24.
Schnoebelen, P.: Revisiting ackermann-hardness for lossy counter machines and reset petri nets. In: Hliněný, P., Kučera, A. (eds.) MFCS 2010. LNCS, vol. 6281, pp. 616–628. Springer, Heidelberg (2010)CrossRef
25.
Stoller, S.D., Yang, P., Gofman, M.I., Ramakrishnan, C.R.: Symbolic reachability analysis for parameterized administrative role-based access control. Comput. Secur. 30(2–3), 148–164 (2011)CrossRef
26.
Tzevelekos, N.: Fresh-register automata. In: POPL 2011, pp. 295–306 (2011)
27.
Tzevelekos, N., Grigore, R.: History-register automata. In: Pfenning, F. (ed.) FOSSACS 2013 (ETAPS 2013). LNCS, vol. 7794, pp. 17–33. Springer, Heidelberg (2013)CrossRef
Metadata
Title
Data Tracking in Parameterized Systems
Author
Giorgio Delzanno
Copyright Year
2016
Book
Trustworthy Global Computing

Print ISBN: 978-3-319-28765-2

Electronic ISBN: 978-3-319-28766-9

Copyright Year: 2016

DOI
https://doi.org/10.1007/978-3-319-28766-9_3

Premium Partner

    Image Credits