By: Eunsuk Kang (eunsuk.kang@berkeley.edu), Aleksandar Milicevic (almili@microsoft.com), and Daniel Jackson (dnj@mit.edu)
Associate Editor: Mehdi Mirakhorli (@MehdiMirakhorli)
Abstraction is one of the most fundamental techniques in software design, but can be a double-edged sword, especially in systems where security is a major concern. Most systems are too complex to reason about all at once, and so developers tend to focus on one aspect of a system at a time, and ignore irrelevant details. However, an attacker need not respect the same abstraction boundaries, and may exploit details across multiple layers of a system.
One well-known example of this type of security risk can be found in OAuth, a popular authorization protocol. Many web-based implementations of OAuth have been shown to be vulnerable to attacks [4], despite the fact that the protocol itself was subjected to rigorous analyses (including formal verification [2][5]). In hindsight, this is not too surprising, since the protocol is a set of abstract rules that omits details about an underlying platform---deliberately so, since it makes the protocol reusable across multiple platforms! At the same time, it is exactly some of these details (e.g., various browser features and interaction with malicious agents on the web) that allowed an attacker to compromise the security guarantees that the protocol is designed to provide.
In general, security is a cross-cutting concern that cannot be easily contained within a single abstraction of a system. A security guarantee established at one layer may no longer hold once the system is elaborated with details during an implementation phase. Currently, it remains the developer’s burden to ensure that the high-level guarantee is preserved in the implementation---a challenging task even for those with security expertise, due to the complexity of modern platforms such as web browsers.
How do we reason about potential attacks across multiple abstractions of a system? Can we anticipate and address such attacks proactively, before building an implementation? How much detail about the underlying platform do we need to include to perform this analysis?
Poirot is a security analysis tool designed to help developers proactively detect what we call cross-layer vulnerabilities [3]. The tool takes three types of inputs: (1) a pair of models that describe a high-level design and a low-level platform, (2) a desired security property (typically expressed over the high-level model), and (3) a representation mapping, which describes how entities from the high-level model are to be represented in terms of their low-level counterparts. Given these inputs, Poirot exhaustively analyzes potential interactions between the two layers and produces scenarios that describe how an attacker may exploit some of these interactions to undermine the security property. The analysis can be carried out incrementally: Starting with an abstract model that represents an initial design of the system, the designer can elaborate a part of the model with a choice of representation, transforming the model into a more detailed one.
A key aspect of Poirot is the representation mapping, which allows the developer to specify decisions about how an abstract design is to be implemented using concrete primitives. For example, when designing an online shopping cart, one may define an operation named Add, which corresponds to the action of adding a new item to a customer’s shopping cart. At the abstract design level, this operation contains two arguments, as shown in Figure 1: the identifier of the item to be added (i), and a token that represents a customer’s credential (t). In order to deploy the shopping application onto the HTTP protocol, our developer must eventually decide how the two parameters from Add are to be mapped to its counterparts in a concrete HTTP request.
In an early design stage, however, the developer may possess only partial knowledge about the system, and some of these decisions may be unknown. Poirot allows the representation mapping to be only partially specified, allowing the developer to express her uncertainty about design decisions and systematically explore different candidate mappings. For instance, Figure 1 depicts a partial mapping specification that lists only the origin and path of the Add URL, leaving unspecified how the item ID and token will be transmitted as part of a request; this, naturally, yields a space of possible mappings, each leading to a different implementation of the shopping cart (and each with its own security vulnerabilities).
Another important part of Poirot is the library of domain models that together describe a platform---collection of generic components, data structures, and libraries that are used to implement an application. In our example, this library would include generic models of various components of the Web, such as a web server, the HTTP protocol, a browser, and its various features (cookie handling, page rendering, scripts, etc.). Once constructed by domain experts, these models should be reusable for analysis of multiple systems in the same domain. Reusability is crucial for Poirot: If each developer had to write these models for every system to be analyzed, it would simply take too much effort! Thanks to our flexible composition mechanism [3], this library is also easily extensible, in that fresh knowledge about a feature or newly discovered vulnerability can be encoded as a separate model and inserted into the library for later use.
Poirot is most effective when applied early in a development process. As a case study, we had an opportunity to work with a startup called HandMe.In, which was building an online system for tracking personal items. In collaboration with the lead developer, we applied Poirot to discover a number of potential security vulnerabilities in the system, resulting in significant changes to the design. In another study, we used Poirot to model and analyze the security of IFTTT, an application that allows an end user to automate web services, and discovered a previously unknown attack that exploited an interaction between the IFTTT protocol and a browser vulnerability called login CSRF. Many of the attacks generated by Poirot exploited system details at multiple levels of abstraction, and would not have been found if the analysis were confined to a single layer.
There are examples of cross-layer vulnerabilities in a number of other domains besides web security. For instance, a program in a high-level language (e.g., Java) may inadvertently expose private data when translated into a low-level representation (bytecode) [1]. We are currently investigating whether Poirot can be applied to these types of domains as well. In addition, we are building an extension that will allow Poirot to not only produce potential vulnerabilities, but also generate a representation mapping that preserves a desired security property across multiple layers, by leveraging techniques from program synthesis.
Read more about Poirot in our FSE paper [3], or try out the tool at https://eskang.github.io/poirot/
References
[1] M. Abadi. Protection in programming language translations. In International Colloquium on Automata, Languages and Programming (ICALP), 1998.
[2] S. Chari, C. S. Jutla, and A. Roy. Universally Composable Security Analysis of OAuth v2.0. IACR Cryptology ePrint Archive, 2011:526, 2011.
[3] E. Kang, A. Milicevic, and D. Jackson. Multi-representational security analysis. In International Symposium on the Foundations of Software Engineering (FSE), 2016.
[4] S. Sun and K. Beznosov. The devil is in the (implementation) details: an empirical analysis of OAuth SSO systems. In ACM Conference on Computer and Communications Security (CCS), 2012.
[5] X. Xu, L. Niu, and B. Meng. Automatic verification of security properties of OAuth 2.0 protocol with cryptoverif in computational model. Information Technology Journal, 12(12):2273, 2013.
Associate Editor: Mehdi Mirakhorli (@MehdiMirakhorli)
Abstraction is one of the most fundamental techniques in software design, but can be a double-edged sword, especially in systems where security is a major concern. Most systems are too complex to reason about all at once, and so developers tend to focus on one aspect of a system at a time, and ignore irrelevant details. However, an attacker need not respect the same abstraction boundaries, and may exploit details across multiple layers of a system.
One well-known example of this type of security risk can be found in OAuth, a popular authorization protocol. Many web-based implementations of OAuth have been shown to be vulnerable to attacks [4], despite the fact that the protocol itself was subjected to rigorous analyses (including formal verification [2][5]). In hindsight, this is not too surprising, since the protocol is a set of abstract rules that omits details about an underlying platform---deliberately so, since it makes the protocol reusable across multiple platforms! At the same time, it is exactly some of these details (e.g., various browser features and interaction with malicious agents on the web) that allowed an attacker to compromise the security guarantees that the protocol is designed to provide.
In general, security is a cross-cutting concern that cannot be easily contained within a single abstraction of a system. A security guarantee established at one layer may no longer hold once the system is elaborated with details during an implementation phase. Currently, it remains the developer’s burden to ensure that the high-level guarantee is preserved in the implementation---a challenging task even for those with security expertise, due to the complexity of modern platforms such as web browsers.
How do we reason about potential attacks across multiple abstractions of a system? Can we anticipate and address such attacks proactively, before building an implementation? How much detail about the underlying platform do we need to include to perform this analysis?
Poirot is a security analysis tool designed to help developers proactively detect what we call cross-layer vulnerabilities [3]. The tool takes three types of inputs: (1) a pair of models that describe a high-level design and a low-level platform, (2) a desired security property (typically expressed over the high-level model), and (3) a representation mapping, which describes how entities from the high-level model are to be represented in terms of their low-level counterparts. Given these inputs, Poirot exhaustively analyzes potential interactions between the two layers and produces scenarios that describe how an attacker may exploit some of these interactions to undermine the security property. The analysis can be carried out incrementally: Starting with an abstract model that represents an initial design of the system, the designer can elaborate a part of the model with a choice of representation, transforming the model into a more detailed one.
 |
| Figure 1: Partial Mapping from abstract Add to HTTP request. |
A key aspect of Poirot is the representation mapping, which allows the developer to specify decisions about how an abstract design is to be implemented using concrete primitives. For example, when designing an online shopping cart, one may define an operation named Add, which corresponds to the action of adding a new item to a customer’s shopping cart. At the abstract design level, this operation contains two arguments, as shown in Figure 1: the identifier of the item to be added (i), and a token that represents a customer’s credential (t). In order to deploy the shopping application onto the HTTP protocol, our developer must eventually decide how the two parameters from Add are to be mapped to its counterparts in a concrete HTTP request.
In an early design stage, however, the developer may possess only partial knowledge about the system, and some of these decisions may be unknown. Poirot allows the representation mapping to be only partially specified, allowing the developer to express her uncertainty about design decisions and systematically explore different candidate mappings. For instance, Figure 1 depicts a partial mapping specification that lists only the origin and path of the Add URL, leaving unspecified how the item ID and token will be transmitted as part of a request; this, naturally, yields a space of possible mappings, each leading to a different implementation of the shopping cart (and each with its own security vulnerabilities).
Another important part of Poirot is the library of domain models that together describe a platform---collection of generic components, data structures, and libraries that are used to implement an application. In our example, this library would include generic models of various components of the Web, such as a web server, the HTTP protocol, a browser, and its various features (cookie handling, page rendering, scripts, etc.). Once constructed by domain experts, these models should be reusable for analysis of multiple systems in the same domain. Reusability is crucial for Poirot: If each developer had to write these models for every system to be analyzed, it would simply take too much effort! Thanks to our flexible composition mechanism [3], this library is also easily extensible, in that fresh knowledge about a feature or newly discovered vulnerability can be encoded as a separate model and inserted into the library for later use.
Poirot is most effective when applied early in a development process. As a case study, we had an opportunity to work with a startup called HandMe.In, which was building an online system for tracking personal items. In collaboration with the lead developer, we applied Poirot to discover a number of potential security vulnerabilities in the system, resulting in significant changes to the design. In another study, we used Poirot to model and analyze the security of IFTTT, an application that allows an end user to automate web services, and discovered a previously unknown attack that exploited an interaction between the IFTTT protocol and a browser vulnerability called login CSRF. Many of the attacks generated by Poirot exploited system details at multiple levels of abstraction, and would not have been found if the analysis were confined to a single layer.
There are examples of cross-layer vulnerabilities in a number of other domains besides web security. For instance, a program in a high-level language (e.g., Java) may inadvertently expose private data when translated into a low-level representation (bytecode) [1]. We are currently investigating whether Poirot can be applied to these types of domains as well. In addition, we are building an extension that will allow Poirot to not only produce potential vulnerabilities, but also generate a representation mapping that preserves a desired security property across multiple layers, by leveraging techniques from program synthesis.
Read more about Poirot in our FSE paper [3], or try out the tool at https://eskang.github.io/poirot/
References
[1] M. Abadi. Protection in programming language translations. In International Colloquium on Automata, Languages and Programming (ICALP), 1998.
[2] S. Chari, C. S. Jutla, and A. Roy. Universally Composable Security Analysis of OAuth v2.0. IACR Cryptology ePrint Archive, 2011:526, 2011.
[3] E. Kang, A. Milicevic, and D. Jackson. Multi-representational security analysis. In International Symposium on the Foundations of Software Engineering (FSE), 2016.
[4] S. Sun and K. Beznosov. The devil is in the (implementation) details: an empirical analysis of OAuth SSO systems. In ACM Conference on Computer and Communications Security (CCS), 2012.
[5] X. Xu, L. Niu, and B. Meng. Automatic verification of security properties of OAuth 2.0 protocol with cryptoverif in computational model. Information Technology Journal, 12(12):2273, 2013.
No comments:
Post a Comment