Utilising K Semantics for Collusion Detection in Android Applications

I.M. Asǎvoae; Hoang Nga Nguyen; M. Roggenbach; Siraj A. Shaikh

doi:10.1007/978-3-319-45943-1_10

Utilising K Semantics for Collusion Detection in Android Applications

I.M. Asǎvoae, Hoang Nga Nguyen, M. Roggenbach, Siraj A. Shaikh

Research output: Chapter in Book/Report/Conference proceeding › Chapter › peer-review

4 Citations (Scopus)

Abstract

The Android OS supports multiple communication methods between apps. This opens the possibility to carry out threats in a collaborative fashion, c.f. the Soundcomber example from 2011. In this paper we demonstrate an effective attempt to detect collusion via model-checking a set of apps utilising the KK framework.

Original language	English
Title of host publication	Critical Systems: Formal Methods and Automated Verification
Editors	Maurice H. Ter Beek, Stefania Gnesi, Alexander Knapp
Publisher	Springer Verlag
Pages	142-149
Volume	9933 LNCS
ISBN (Print)	978-3-319-45942-4
DOIs	https://doi.org/10.1007/978-3-319-45943-1_10
Publication status	Published - Sept 2016
Event	Joint 21st International Workshop on Formal Methods for Industrial Critical Systems and 16th International Workshop on Automated Verification of Critical Systems - Pisa, Italy Duration: 26 Sept 2016 → 28 Sept 2016

Conference

Conference	Joint 21st International Workshop on Formal Methods for Industrial Critical Systems and 16th International Workshop on Automated Verification of Critical Systems
Abbreviated title	FMICS-AVoCS 2016
Country/Territory	Italy
City	Pisa
Period	26/09/16 → 28/09/16

Bibliographical note

This book chapter/conference paper is not available on the repository. The paper was given at the Joint 21st International Workshop on Formal Methods for Industrial Critical Systems and 16th International Workshop on Automated Verification of Critical Systems, FMICS-AVoCS 2016, Pisa, Italy, September 26-28, 2016

Keywords

Logics and Meanings of Programs
Programming Languages
Compilers
Interpreters
Software Engineering
Special Purpose and Application-Based Systems
Mathematical Logic and Formal Languages

Access to Document

10.1007/978-3-319-45943-1_10

Cite this

Utilising K Semantics for Collusion Detection in Android Applications. / Asǎvoae, I.M.; Nguyen, Hoang Nga; Roggenbach, M. et al.

Critical Systems: Formal Methods and Automated Verification. ed. / Maurice H. Ter Beek; Stefania Gnesi; Alexander Knapp. Vol. 9933 LNCS Springer Verlag, 2016. p. 142-149.

Research output: Chapter in Book/Report/Conference proceeding › Chapter › peer-review

Asǎvoae, IM, Nguyen, HN, Roggenbach, M & Shaikh, SA 2016, Utilising K Semantics for Collusion Detection in Android Applications. in MHT Beek, S Gnesi & A Knapp (eds), Critical Systems: Formal Methods and Automated Verification. vol. 9933 LNCS, Springer Verlag, pp. 142-149, Joint 21st International Workshop on Formal Methods for Industrial Critical Systems and 16th International Workshop on Automated Verification of Critical Systems, Pisa, Italy, 26/09/16. https://doi.org/10.1007/978-3-319-45943-1_10

@inbook{e679d3f89a754f3883707ae4c7c3376a,

title = "Utilising K Semantics for Collusion Detection in Android Applications",

abstract = "The Android OS supports multiple communication methods between apps. This opens the possibility to carry out threats in a collaborative fashion, c.f. the Soundcomber example from 2011. In this paper we demonstrate an effective attempt to detect collusion via model-checking a set of apps utilising the KK framework.",

keywords = "Logics and Meanings of Programs, Programming Languages, Compilers, Interpreters, Software Engineering, Special Purpose and Application-Based Systems, Mathematical Logic and Formal Languages",

author = "I.M. Asǎvoae and Nguyen, {Hoang Nga} and M. Roggenbach and Shaikh, {Siraj A.}",

note = "This book chapter/conference paper is not available on the repository. The paper was given at the Joint 21st International Workshop on Formal Methods for Industrial Critical Systems and 16th International Workshop on Automated Verification of Critical Systems, FMICS-AVoCS 2016, Pisa, Italy, September 26-28, 2016; Joint 21st International Workshop on Formal Methods for Industrial Critical Systems and 16th International Workshop on Automated Verification of Critical Systems, FMICS-AVoCS 2016 ; Conference date: 26-09-2016 Through 28-09-2016",

year = "2016",

month = sep,

doi = "10.1007/978-3-319-45943-1_10",

language = "English",

isbn = "978-3-319-45942-4",

volume = "9933 LNCS",

pages = "142--149",

editor = "Beek, {Maurice H. Ter} and Stefania Gnesi and Alexander Knapp",

booktitle = "Critical Systems: Formal Methods and Automated Verification",

publisher = "Springer Verlag",

address = "Austria",

}

TY - CHAP

T1 - Utilising K Semantics for Collusion Detection in Android Applications

AU - Asǎvoae, I.M.

AU - Nguyen, Hoang Nga

AU - Roggenbach, M.

AU - Shaikh, Siraj A.

N1 - This book chapter/conference paper is not available on the repository. The paper was given at the Joint 21st International Workshop on Formal Methods for Industrial Critical Systems and 16th International Workshop on Automated Verification of Critical Systems, FMICS-AVoCS 2016, Pisa, Italy, September 26-28, 2016

PY - 2016/9

Y1 - 2016/9

N2 - The Android OS supports multiple communication methods between apps. This opens the possibility to carry out threats in a collaborative fashion, c.f. the Soundcomber example from 2011. In this paper we demonstrate an effective attempt to detect collusion via model-checking a set of apps utilising the KK framework.

AB - The Android OS supports multiple communication methods between apps. This opens the possibility to carry out threats in a collaborative fashion, c.f. the Soundcomber example from 2011. In this paper we demonstrate an effective attempt to detect collusion via model-checking a set of apps utilising the KK framework.

KW - Logics and Meanings of Programs

KW - Programming Languages

KW - Compilers

KW - Interpreters

KW - Software Engineering

KW - Special Purpose and Application-Based Systems

KW - Mathematical Logic and Formal Languages

U2 - 10.1007/978-3-319-45943-1_10

DO - 10.1007/978-3-319-45943-1_10

M3 - Chapter

SN - 978-3-319-45942-4

VL - 9933 LNCS

SP - 142

EP - 149

BT - Critical Systems: Formal Methods and Automated Verification

A2 - Beek, Maurice H. Ter

A2 - Gnesi, Stefania

A2 - Knapp, Alexander

PB - Springer Verlag

T2 - Joint 21st International Workshop on Formal Methods for Industrial Critical Systems and 16th International Workshop on Automated Verification of Critical Systems

Y2 - 26 September 2016 through 28 September 2016

ER -

Utilising K Semantics for Collusion Detection in Android Applications

Abstract

Conference

Bibliographical note

Keywords

Access to Document

Fingerprint

Cite this