SeMA: Extending and Analyzing Storyboards to Develop Secure Android Apps
Authors:
Joydeep Mitra,
Venkatesh-Prasad Ranganath,
Torben Amtoft,
Mike Higgins
Abstract:
Mobile apps provide various critical services, such as banking, communication, and healthcare. To this end, they have access to our personal information and have the ability to perform actions on our behalf. Hence, securing mobile apps is crucial to ensuring the privacy and safety of its users.
Recent research efforts have focused on develo** solutions to secure mobile ecosystems (i.e., app pl…
▽ More
Mobile apps provide various critical services, such as banking, communication, and healthcare. To this end, they have access to our personal information and have the ability to perform actions on our behalf. Hence, securing mobile apps is crucial to ensuring the privacy and safety of its users.
Recent research efforts have focused on develo** solutions to secure mobile ecosystems (i.e., app platforms, apps, and app stores), specifically in the context of detecting vulnerabilities in Android apps. Despite this attention, known vulnerabilities are often found in mobile apps, which can be exploited by malicious apps to harm the user. Further, fixing vulnerabilities after develo** an app has downsides in terms of time, resources, user inconvenience, and information loss.
In an attempt to address this concern, we have developed SeMA, a mobile app development methodology that builds on existing mobile app design artifacts such as storyboards. With SeMA, security is a first-class citizen in an app's design -- app designers and developers can collaborate to specify and reason about the security properties of an app at an abstract level without being distracted by implementation level details. Our realization of SeMA using Android Studio tooling demonstrates the methodology is complementary to existing design and development practices. An evaluation of the effectiveness of SeMA shows the methodology can detect and help prevent 49 vulnerabilities known to occur in Android apps. Further, a usability study of the methodology involving ten real-world developers shows the methodology is likely to reduce the development time and help developers uncover and prevent known vulnerabilities while designing apps.
△ Less
Submitted 10 March, 2024; v1 submitted 27 January, 2020;
originally announced January 2020.
A Semantics for Probabilistic Control-Flow Graphs
Authors:
Torben Amtoft,
Anindya Banerjee
Abstract:
This article develops a novel operational semantics for probabilistic control-flow graphs (pCFGs) of probabilistic imperative programs with random assignment and "observe" (or conditioning) statements. The semantics transforms probability distributions (on stores) as control moves from one node to another in pCFGs. We relate this semantics to a standard, expectation-transforming, denotational sema…
▽ More
This article develops a novel operational semantics for probabilistic control-flow graphs (pCFGs) of probabilistic imperative programs with random assignment and "observe" (or conditioning) statements. The semantics transforms probability distributions (on stores) as control moves from one node to another in pCFGs. We relate this semantics to a standard, expectation-transforming, denotational semantics of structured probabilistic imperative programs, by translating structured programs into (unstructured) pCFGs, and proving adequacy of the translation. This shows that the operational semantics can be used without loss of information, and is faithful to the "intended" semantics and hence can be used to reason about, for example, the correctness of transformations (as we do in a companion article).
△ Less
Submitted 6 November, 2017;
originally announced November 2017.
A Theory of Slicing for Probabilistic Control-Flow Graphs
Authors:
Torben Amtoft,
Anindya Banerjee
Abstract:
We present a theory for slicing probabilistic imperative programs -- containing random assignments, and ``observe'' statements (for conditioning) -- represented as probabilistic control-flow graphs (pCFGs) whose nodes modify probability distributions.
We show that such a representation allows direct adaptation of standard machinery such as data and control dependence, postdominators, relevant va…
▽ More
We present a theory for slicing probabilistic imperative programs -- containing random assignments, and ``observe'' statements (for conditioning) -- represented as probabilistic control-flow graphs (pCFGs) whose nodes modify probability distributions.
We show that such a representation allows direct adaptation of standard machinery such as data and control dependence, postdominators, relevant variables, etc to the probabilistic setting. We separate the specification of slicing from its implementation: first we develop syntactic conditions that a slice must satisfy; next we prove that any such slice is semantically correct; finally we give an algorithm to compute the least slice. To generate smaller slices, we may in addition take advantage of knowledge that certain loops will terminate (almost) always.
A key feature of our syntactic conditions is that they involve two disjoint slices such that the variables of one slice are probabilistically independent of the variables of the other. This leads directly to a proof of correctness of probabilistic slicing. In a companion article we show adequacy of the semantics of pCFGs with respect to the standard semantics of structured probabilistic programs.
△ Less
Submitted 6 November, 2017;
originally announced November 2017.
