Software Model Checking for Mobile Security – Collusion Detection in \mathbb {K}K

DOI10.1007/978-3-319-94111-0_1MaRDI QIDQ5883569zbMATH OpenOpenAlexFDO

Authors Irina Măriuca Asăvoae, Hoang Nga Nguyen, Markus Roggenbach

Publication date 21 March 2023

Published in Model Checking Software (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-94111-0_1

zbMATH Keywords

model checkingmobile securityAndroid

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Semantics in the theory of computing (68Q55) Theory of operating systems (68N25)

Recommendations

• Formal analysis of Android's permission-based security model
• Presenting risks introduced by Android application permissions in a user-friendly way
• Verifying Android's permission model
• A Markov adversary model to detect vulnerable iOS devices and vulnerabilities in iOS apps
• Formal Enforcement of Security Policies on Parallel Systems with Risk Integration

Cites work

• scientific article; zbMATH DE number 1324833 (Why is no real title available?)
• All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
• An overview of the K semantic framework
• Combining model checking and data-flow analysis
• From rewriting logic, to programming language semantics, to program verification
• K-Maude: a rewriting based tool for semantics of programming languages

Cited in

(10)

• Once root always a threat: analyzing the security threats of Android permission system
• Presenting risks introduced by Android application permissions in a user-friendly way
• A Markov adversary model to detect vulnerable iOS devices and vulnerabilities in iOS apps
• Verifying Android's permission model
• A model checking-based approach for security policy verification of mobile systems
• Protecting data on android platform against privilege escalation attack
• A secure architecture for operating system-level virtualization on mobile devices
• A certified reference validation mechanism for the permission model of Android
• Formal analysis of Android's permission-based security model
• Cochecker: detecting capability and sensitive data leaks from component chains in Android

Describes a project that uses

Uses Software

• FlowDroid
• K-Java
• K-Maude
• K tool
• Maude

This page was built for publication: Software Model Checking for Mobile Security – Collusion Detection in $$\mathbb {K}$$K

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5883569)