Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
An Exercise in Mathematical Engineering: Stating and Proving Kuratowski Theorem Kapitel lesen Erstes Kapitel lesen

2015 | OriginalPaper | Buchkapitel

Verifying Android’s Permission Model

verfasst von : Gustavo Betarte, Juan Diego Campo, Carlos Luna, Agustín Romano

Erschienen in: Theoretical Aspects of Computing - ICTAC 2015

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

In the Android platform application security is built primarily upon a system of permissions which specify restrictions on the operations a particular process can perform. Several analyses have recently been carried out concerning the security of the Android system. Few of them, however, pay attention to the formal aspects of the permission enforcing framework. In this work we present a comprehensive formal specification of an idealized formulation of Android’s permission model and discuss several security properties that have been verified using the proof assistant Coq.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

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!

Jetzt informieren

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!

Jetzt informieren

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!

Jetzt informieren
Vorheriges Kapitel Multi-rate System Design Through Integrating Synchronous Components
Nächstes Kapitel CSP and Kripke Structures
Fußnoten
1
We omit the formal definition of validState due to space constraints.
 
2
In particular, ic can read/write the resource pointed by u in cp if ic has permission due to a delegation via intents.
 
3
In [20] we prove a similar result for action \(\mathtt {write}\).
 
Literatur
1.
2.
3.
4.
5.
6.
7.
8.
9.
10.
Armando, A., Costa, G., Merlo, A.: Formal modeling and reasoning about the android security framework. In: 7th International Symposium on Trustworthy Global Computing (2012)
11.
Zanella Béguelin, S., Betarte, G., Luna, C.: A formal specification of the MIDP 2.0 security model. In: Dimitrakos, T., Martinelli, F., Ryan, P.Y.A., Schneider, S. (eds.) FAST 2006. LNCS, vol. 4691, pp. 220–234. Springer, Heidelberg (2007) CrossRef
12.
Bertot, Y., Castran, P.: Interactive Theorem Proving and Program Development. Coq’Art: The Calculus of Inductive Constructions. Texts in theoretical computer science. Springer, Berlin (2004) CrossRef
13.
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
14.
Chaudhuri, A.: Language-based security on android. In: Proceedings of the ACM SIGPLAN Fourth Workshop on Programming Languages and Analysis for Security, PLAS 2009, pp. 1–7. ACM, New York, NY, USA (2009)
15.
Conti, M., Nguyen, V.T.N., Crispo, B.: CRePE: context-related policy enforcement for android. In: Burmester, M., Tsudik, G., Magliveras, S., Ilic, I. (eds.) ISC 2010. LNCS, vol. 6531, pp. 331–345. Springer, Heidelberg (2011) CrossRef
16.
Davi, L., Dmitrienko, A., Sadeghi, A.-R., Winandy, M.: Privilege escalation attacks on android. In: Burmester, M., Tsudik, G., Magliveras, S., Ilic, I. (eds.) ISC 2010. LNCS, vol. 6531, pp. 346–360. Springer, Heidelberg (2011) CrossRef
17.
Felt, A.P., Chin, E., Hanna, S., Dawn Song, and David Wagner. Android permissions demystified. In: Proceedings of the 18th ACM conference on Computer and communications security, CCS 2011, pages 627–638. ACM, New York, NY, USA (2011)
18.
Felt, A.P., Wang, H.J., Moshchuk, A., Hanna, S., Chin, E.: Permission re-delegation: Attacks and defenses. In: USENIX Security Symposium. USENIX Association (2011)
19.
Fragkaki, E., Bauer, L., Jia, L., Swasey, D.: Modeling and enhancing android’s permission system. In: Foresti, S., Yung, M., Martinelli, F. (eds.) ESORICS 2012. LNCS, vol. 7459, pp. 1–18. Springer, Heidelberg (2012) CrossRef
20.
21.
Nauman, M., Khan, S., Zhang, X.: Apex: extending android permission model and enforcement with user-defined runtime constraints. In: Proceedings of the 5th ACM Symposium on Information, Computer and Communications Security, ASIACCS 2010, pp. 328–332. ACM, New York, NY, USA (2010)
22.
23.
Paulin-Mohring, C.: Inductive definitions in the system Coq rules and properties. In: Bezem, M., Groote, J.F. (eds.) TLCA 1993. LNCS, vol. 664, pp. 328–345. Springer, Heidelberg (1993) CrossRef
24.
Shin, W., Kiyomoto, S., Fukushima, K., Tanaka,T.: A formal model to analyze the permission authorization and enforcement in the android framework. In: Proceedings of the 2010 IEEE Second International Conference on Social Computing, pp. 944–951, Washington, DC, USA, 2010. IEEE Computer Society
25.
Six, J.: Application Security for the Android Platform. O’Reilly Media, San Francisco (2011)
26.
Team, The Coq Development: The Coq Proof Assistant Reference Manual - Version V8, 4 (2012)
Metadaten
Titel
Verifying Android’s Permission Model
verfasst von
Gustavo Betarte
Juan Diego Campo
Carlos Luna
Agustín Romano
Copyright-Jahr
2015
Buch
Theoretical Aspects of Computing - ICTAC 2015

Print ISBN: 978-3-319-25149-3

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

Copyright-Jahr: 2015

DOI
https://doi.org/10.1007/978-3-319-25150-9_28