An Operational Semantics for Android Applications

2016 ◽  
pp. 100-114 ◽  
Author(s):  
Mohamed A. El-Zawawy
Keyword(s):  
Operational Semantics ◽  
Android Applications

scholarly journals Smali+: An Operational Semantics for Low-Level Code Generated from Reverse Engineering Android Applications

Information ◽  
2020 ◽  
Vol 11 (3) ◽  
pp. 130 ◽  
Author(s):  
Marwa Ziadia ◽  
Jaouhar Fattahi ◽  
Mohamed Mejri ◽  
Emil Pricop
Keyword(s):  
Reverse Engineering ◽  
Operational Semantics ◽  
Global Market ◽  
High Rate ◽  
Formal Approach ◽  
Detection Techniques ◽  
Art Works ◽  
Formal Basis ◽  
Android Applications ◽  
Natural Means

Today, Android accounts for more than 80% of the global market share. Such a high rate makes Android applications an important topic that raises serious questions about its security, privacy, misbehavior and correctness. Application code analysis is obviously the most appropriate and natural means to address these issues. However, no analysis could be led with confidence in the absence of a solid formal foundation. In this paper, we propose a full-fledged formal approach to build the operational semantics of a given Android application by reverse-engineering its assembler-type code, called Smali. We call the new formal language Smali + . Its semantics consist of two parts. The first one models a single-threaded program, in which a set of main instructions is presented. The second one presents the semantics of a multi-threaded program which is an important feature in Android that has been glossed over in the-state-of-the-art works. All multi-threading essentials such as scheduling, threads communication and synchronization are considered in these semantics. The resulting semantics, forming Smali + , are intended to provide a formal basis for developing security enforcement, analysis and misbehaving detection techniques for Android applications.

scholarly journals Specifying and Executing User Agents in an Environment of Reasoning and RESTful Systems Using the Guard-Stage-Milestone Approach

2021 ◽  
Author(s):  
Tobias Käfer ◽  
Benjamin Jochum ◽  
Nico Aßfalg ◽  
Leonard Nürnberg
Keyword(s):  
Linked Data ◽  
Operational Semantics ◽  
Workflow Management ◽  
Management Systems ◽  
Workflow Management Systems ◽  
The Web

AbstractFor Read-Write Linked Data, an environment of reasoning and RESTful interaction, we investigate the use of the Guard-Stage-Milestone approach for specifying and executing user agents. We present an ontology to specify user agents. Moreover, we give operational semantics to the ontology in a rule language that allows for executing user agents on Read-Write Linked Data. We evaluate our approach formally and regarding performance. Our work shows that despite different assumptions of this environment in contrast to the traditional environment of workflow management systems, the Guard-Stage-Milestone approach can be transferred and successfully applied on the web of Read-Write Linked Data.

scholarly journals Persistent Stochastic Non-Interference

2021 ◽  
Vol 181 (1) ◽  
pp. 1-35
Author(s):  
Jane Hillston ◽  
Andrea Marin ◽  
Carla Piazza ◽  
Sabina Rossi
Keyword(s):  
Process Algebra ◽  
Operational Semantics ◽  
Evaluation Process ◽  
Decision Algorithm ◽  
Secure Systems ◽  
Information Flow Security ◽  
Structural Operational Semantics ◽  
Timing Properties ◽  
Functional Point ◽  
Security Property

In this paper, we study an information flow security property for systems specified as terms of a quantitative Markovian process algebra, namely the Performance Evaluation Process Algebra (PEPA). We propose a quantitative extension of the Non-Interference property used to secure systems from the functional point view by assuming that the observers are able to measure also the timing properties of the system, e.g., the response time of certain actions or its throughput. We introduce the notion of Persistent Stochastic Non-Interference (PSNI) based on the idea that every state reachable by a process satisfies a basic Stochastic Non-Interference (SNI) property. The structural operational semantics of PEPA allows us to give two characterizations of PSNI: one based on a bisimulation-like equivalence relation inducing a lumping on the underlying Markov chain, and another one based on unwinding conditions which demand properties of individual actions. These two different characterizations naturally lead to efficient methods for the verification and construction of secure systems. A decision algorithm for PSNI is presented and an application of PSNI to a queueing system is discussed.

scholarly journals Building Standardized and Secure Mobile Health Services Based on Social Media

Electronics ◽  
2020 ◽  
Vol 9 (12) ◽  
pp. 2208
Author(s):  
Jesús D. Trigo ◽  
Óscar J. Rubio ◽  
Miguel Martínez-Espronceda ◽  
Álvaro Alesanco ◽  
José García ◽  
...  
Keyword(s):  
Social Media ◽  
Mobile Devices ◽  
Mobile Health ◽  
Healthcare Services ◽  
Small Scale ◽  
Proof Of Concept ◽  
Privacy And Security ◽  
Health Level 7 ◽  
Information Embedding ◽  
Android Applications

Mobile devices and social media have been used to create empowering healthcare services. However, privacy and security concerns remain. Furthermore, the integration of interoperability biomedical standards is a strategic feature. Thus, the objective of this paper is to build enhanced healthcare services by merging all these components. Methodologically, the current mobile health telemonitoring architectures and their limitations are described, leading to the identification of new potentialities for a novel architecture. As a result, a standardized, secure/private, social-media-based mobile health architecture has been proposed and discussed. Additionally, a technical proof-of-concept (two Android applications) has been developed by selecting a social media (Twitter), a security envelope (open Pretty Good Privacy (openPGP)), a standard (Health Level 7 (HL7)) and an information-embedding algorithm (modifying the transparency channel, with two versions). The tests performed included a small-scale and a boundary scenario. For the former, two sizes of images were tested; for the latter, the two versions of the embedding algorithm were tested. The results show that the system is fast enough (less than 1 s) for most mHealth telemonitoring services. The architecture provides users with friendly (images shared via social media), straightforward (fast and inexpensive), secure/private and interoperable mHealth services.

scholarly journals Dynamic game semantics

2020 ◽  
pp. 1-60
Author(s):  
Norihiro Yamada ◽  
Samson Abramsky
Keyword(s):  
Programming Languages ◽  
Functional Programming ◽  
Operational Semantics ◽  
Dynamic Game ◽  
Standard Interpretation ◽  
Functional Programming Languages ◽  
Game Semantics ◽  
Wide Range ◽  
Cartesian Closed Categories ◽  
Cartesian Closed

Abstract The present work achieves a mathematical, in particular syntax-independent, formulation of dynamics and intensionality of computation in terms of games and strategies. Specifically, we give game semantics of a higher-order programming language that distinguishes programmes with the same value yet different algorithms (or intensionality) and the hiding operation on strategies that precisely corresponds to the (small-step) operational semantics (or dynamics) of the language. Categorically, our games and strategies give rise to a cartesian closed bicategory, and our game semantics forms an instance of a bicategorical generalisation of the standard interpretation of functional programming languages in cartesian closed categories. This work is intended to be a step towards a mathematical foundation of intensional and dynamic aspects of logic and computation; it should be applicable to a wide range of logics and computations.

An operational semantics for parallel lazy evaluation

2000 ◽  
Vol 35 (9) ◽  
pp. 162-173 ◽  
Author(s):  
Clem Baker-Finch ◽  
David J. King ◽  
Phil Trinder
Keyword(s):  
Operational Semantics ◽  
Lazy Evaluation
Sign in / Sign up

Export Citation Format

Share Document