Home automation platforms such as Samsung SmartThings or Google Nest represent the next step in the evolution of operating systems. Their general security architectures adopt core design elements from smartphone OSes, such as providing APIs to integrate third-party applications or apps, and using permissions to constrain the damage from malicious/misconfigured apps.
However, three central characteristics of home automation result in novel challenges for secure OS design, as well as security, safety, and privacy analyses:
Our goal is to develop a realistic and long-lasting characterization of the automated home by demystifying each of the three factors, and hence lay the groundwork for building practical analysis frameworks and defenses for home automation. We expect such a characterization to be instrumental for security analyses in years to come, as operating systems evolve further to increasingly interact with users their physical environments in smart homes, communities, and cities.
Grants: W&M Faculty Summer Research Award 2019-20
Towards a Natural Perspective of Smart Homes for Practical Security and Safety Analyses
Sunil Manandhar, Kevin Moran, Kaushal Kafle, Ruhao Tang, Denys Poshyvanyk, and Adwait Nadkarni
IEEE S&P (Oakland) 2020 (to appear)
A Study of Data Store-based Home Automation
Kaushal Kafle, Kevin Moran, Sunil Manandhar, Adwait Nadkarni, and Denys Poshyvanyk
ACM CODASPY 2019 (Best Paper Award)
This project evaluates the practical implications of the decades-old tradeoff between soundness and precision. The analysis is sound if it identifies every instance of the target behavior (e.g., SSL use vulnerabilities or data leaks) in the application being analyzed. Further, the analysis is precise if every instance of the target behavior that it has identified is true (i.e., if there are no false positives).
Intuitively, there is a conflict between these two properties: sound analysis requires the technique to over-approximate (i.e., consider instances of target behaviors that may not be executed in reality, which deteriorates precision). Static security analysis techniques used for analyzing applications are not exempt from this paradox, as while they may be theoretically sound , they often make unsound choices in practice. Such techniques can be termed as soundy, i.e., consisting of a core set of sound security decisions accompanied by unsound choices with unknown implications.
To address this fundamental problem, we propose mutation-based Soundness Evaluation (μSE, read as ”muse”) of Android static analysis techniques, which aims at enabling evaluation of Android static analysis tools by relying on the technique of mutation analysis in software engineering. Our initial exploration has led to the discovery of 13 flaws in FlowDroid, one of the most popular data leak detection tools for Android apps, and 12 flaws in other popular tools (Argus, HornDroid). We are currently working on leveraging μSE to build better tools, as well as to automate the evaluation for several other security goals, such as detecting SSL misuse.
Discovering Flaws in Security-Focused Static Analysis Tools for Android using Systematic Mutation
Richard Bonett, Kaushal Kafle, Kevin Moran, Adwait Nadkarni, and Denys Poshyvanyk
USENIX Security 2018