| 1. |
- Ahmadian, Amir M., et al.
(författare)
-
Dynamic Policies Revisited
- 2022
-
Ingår i: Proceedings - 7th IEEE European Symposium on Security and Privacy, Euro S and P 2022. - : Institute of Electrical and Electronics Engineers (IEEE). ; , s. 448-466
-
Konferensbidrag (refereegranskat)abstract
- Information flow control and dynamic policies is a difficult relationship yet to be fully understood. While dynamic policies are a natural choice in many real-world applications that downgrade and upgrade the sensitivity of information, understanding the meaning of security in this setting is challenging. In this paper we revisit the knowledge-based security conditions to reinstate a simple and intuitive security condition for dynamic policies: A program is secure if at any point during the execution the attacker's knowledge is in accordance with the active security policy at that execution point. Our key observation is the new notion of policy consistency to prevent policy changes whenever an attacker is already in possession of the information that the new policy intends to protect. We use this notion to study a range of realistic attackers including the perfect recall attacker, bounded attackers, and forgetful attackers, and their relationship. Importantly, our new security condition provides a clean connection between the dynamic policy and the underlying attacker model independently of the specific use case. We illustrate this by considering the different facets of dynamic policies in our framework. On the verification side, we design and implement DynCoVer, a tool for checking dynamic information-flow policies for Java programs via symbolic execution and SMT solving. Our verification operates by first extracting a graph of program dependencies and then visiting the graph to check dynamic policies for a range of attackers. We evaluate the effectiveness and efficiency of DyncoVeron a benchmark of use cases from the literature and designed by ourselves, as well as the case study of a social network. The results show that DynCoVer can analyze small but intricate programs indicating that it can help verify security-critical parts of Java applications. We release Dyncover publicly to support open science and encourage researchers to explore the topic further.
|
|
| 2. |
|
|
| 3. |
- Ahmadpanah, Seyed Mohammad Mehdi, 1996, et al.
(författare)
-
SandTrap : Securing javascript-driven trigger-action platforms
- 2021
-
Ingår i: Proceedings of the 30th USENIX Security Symposium. - : USENIX Association. - 9781939133243 ; , s. 2899-2916
-
Konferensbidrag (refereegranskat)abstract
- Trigger-Action Platforms (TAPs) seamlessly connect a wide variety of otherwise unconnected devices and services, ranging from IoT devices to cloud services and social networks. TAPs raise critical security and privacy concerns because a TAP is effectively a “person-in-the-middle” between trigger and action services. Third-party code, routinely deployed as “apps” on TAPs, further exacerbates these concerns. This paper focuses on JavaScript-driven TAPs. We show that the popular IFTTT and Zapier platforms and an open-source alternative Node-RED are susceptible to attacks ranging from exfiltrating data from unsuspecting users to taking over the entire platform. We report on the changes by the platforms in response to our findings and present an empirical study to assess the implications for Node-RED. Motivated by the need for a secure yet flexible way to integrate third-party JavaScript apps, we propose SandTrap, a novel JavaScript monitor that securely combines the Node.js vm module with fully structural proxy-based two-sided membranes to enforce fine-grained access control policies. To aid developers, SandTrap includes a policy generation mechanism. We instantiate SandTrap to IFTTT, Zapier, and Node-RED and illustrate on a set of benchmarks how SandTrap enforces a variety of policies while incurring a tolerable runtime overhead.
|
|
| 4. |
- Ahmadpanah, Seyed Mohammad Mehdi, 1996, et al.
(författare)
-
Securing Node-RED Applications
- 2021
-
Ingår i: Protocols, Strands, and LogicEssays Dedicated to Joshua Guttman on the Occasion of his 66.66th Birthday. - Cham : Springer Science and Business Media Deutschland GmbH. ; , s. 1-21, s. 1-21, s. 1-21
-
Konferensbidrag (refereegranskat)abstract
- Trigger-Action Platforms (TAPs) play a vital role in fulfilling the promise of the Internet of Things (IoT) by seamlessly connecting otherwise unconnected devices and services. While enabling novel and exciting applications across a variety of services, security and privacy issues must be taken into consideration because TAPs essentially act as persons-in-the-middle between trigger and action services. The issue is further aggravated since the triggers and actions on TAPs are mostly provided by third parties extending the trust beyond the platform providers. Node-RED, an open-source JavaScript-driven TAP, provides the opportunity for users to effortlessly employ and link nodes via a graphical user interface. Being built upon Node.js, third-party developers can extend the platform’s functionality through publishing nodes and their wirings, known as flows. This paper proposes an essential model for Node-RED, suitable to reason about nodes and flows, be they benign, vulnerable, or malicious. We expand on attacks discovered in recent work, ranging from exfiltrating data from unsuspecting users to taking over the entire platform by misusing sensitive APIs within nodes. We present a formalization of a runtime monitoring framework for a core language that soundly and transparently enforces fine-grained allowlist policies at module-, API-, value-, and context-level. We introduce the monitoring framework for Node-RED that isolates nodes while permitting them to communicate via well-defined API calls complying with the policy specified for each node.
|
|
| 5. |
- Balliu, Musard
(författare)
-
A Logic for Information Flow Analysis of Distributed Programs
- 2013
-
Ingår i: Secure IT Systems. - Berlin, Heidelberg : Springer Berlin/Heidelberg. - 9783642414886 ; , s. 84-99
-
Konferensbidrag (refereegranskat)abstract
- Securing communication in large scale distributed systems is an open problem. When multiple principals exchange sensitive information over a network, security and privacy issues arise immediately. For instance, in an online auction system we may want to ensure that no bidder knows the bids of any other bidder before the auction is closed. Such systems are typically interactive/reactive and communication is mostly asynchronous, lossy or unordered. Language-based security provides language mechanisms for enforcing end-to-end security. However, with few exceptions, previous research has mainly focused on relational or synchronous models, which are generally not suitable for distributed systems. This paper proposes a general knowledge-based account of possibilistic security from a language perspective and shows how existing trace-based conditions fit in. A syntactic characterization of these conditions, given by an epistemic temporal logic, shows that existing model checking tools can be used to enforce security.
|
|
| 6. |
- Balliu, Musard, et al.
(författare)
-
A weakest precondition approach to active attacks analysis
- 2009
-
Ingår i: PLAS'09. - New York, NY, USA : ACM. - 9781605586458 ; , s. 59-71
-
Konferensbidrag (refereegranskat)abstract
- Information flow controls can be used to protect both data confidentiality and data integrity. The certification of the security degree of a program that runs in untrusted environments still remains an open problem in language-based security. The notion of robustness asserts that an active attacker, who can modify program code in some fixed points (holes), is not able to disclose more private information than a passive attacker, who merely observes public data. In this paper, we extend a method recently proposed for checking declassified non-interference in presence of passive attackers only, in order to check robustness by means of the weakest precondition semantics. In particular, this semantics simulates the kind of analysis that can be performed by an attacker, i.e., from the public output towards the private input. The choice of the semantics lets us distinguish between different attacks models. In this paper, we also introduce relative robustness that is a relaxed notion of robustness for restricted classes of attacks.
|
|
| 7. |
- Balliu, Musard, et al.
(författare)
-
A Weakest Precondition Approach to Robustness
- 2010
-
Ingår i: Lecture Notes in Computer Science. - Berlin, Heidelberg : Springer Berlin Heidelberg. - 0302-9743 .- 1611-3349. ; 6340:PART 1, s. 261-297
-
Tidskriftsartikel (refereegranskat)abstract
- With the increasing complexity of information management computer systems, security becomes a real concern. E-government, web-based financial transactions or military and health care information systems are only a few examples where large amount of information can reside on different hosts distributed worldwide. It is clear that any disclosure or corruption of confidential information in these contexts can result fatal. Information flow controls constitute an appealing and promising technology to protect both data confidentiality and data integrity. The certification of the security degree of a program that runs in untrusted environments still remains an open problem in the area of language-based security. Robustness asserts that an active attacker, who can modify program code in some fixed points (holes), is unable to disclose more private information than a passive attacker, who merely observes unclassified data. In this paper, we extend a method recently proposed for checking declassified non-interference in presence of passive attackers only, in order to check robustness by means of weakest precondition semantics. In particular, this semantics simulates the kind of analysis that can be performed by an attacker, i.e., from public output towards private input. The choice of semantics allows us to distinguish between different attacks models and to characterize the security of applications in different scenarios. Our results are sound to address confidentiality and integrity of software running in untrusted environments where different actors can distrust one another. For instance, a web server can be attacked by a third party in order to steal a session cookie or hijack clients to a fake web page.
|
|
| 8. |
- Balliu, Musard, et al.
(författare)
-
Automating Information Flow Analysis of Low Level Code
- 2014
-
Ingår i: Proceedings of CCS’14, November 3–7, 2014, Scottsdale, Arizona, USA. - New York, NY, USA : Association for Computing Machinery (ACM). - 9781450329576
-
Konferensbidrag (refereegranskat)abstract
- Low level code is challenging: It lacks structure, it uses jumps and symbolic addresses, the control ow is often highly optimized, and registers and memory locations may be reused in ways that make typing extremely challenging. Information ow properties create additional complications: They are hyperproperties relating multiple executions, and the possibility of interrupts and concurrency, and use of devices and features like memory-mapped I/O requires a departure from the usual initial-state nal-state account of noninterference. In this work we propose a novel approach to relational verication for machine code. Verication goals are expressed as equivalence of traces decorated with observation points. Relational verication conditions are propagated between observation points using symbolic execution, and discharged using rst-order reasoning. We have implemented an automated tool that integrates with SMT solvers to automate the verication task. The tool transforms ARMv7 binaries into an intermediate, architecture-independent format using the BAP toolset by means of a veried translator. We demonstrate the capabilities of the tool on a separation kernel system call handler, which mixes hand-written assembly with gcc-optimized output, a UART device driver and a crypto service modular exponentiation routine.
|
|
| 9. |
- Balliu, Musard, et al.
(författare)
-
Challenges of Producing Software Bill of Materials for Java
- 2023
-
Ingår i: IEEE Security and Privacy. - : Institute of Electrical and Electronics Engineers (IEEE). - 1540-7993 .- 1558-4046. ; 21:6, s. 12-23
-
Tidskriftsartikel (refereegranskat)abstract
- Software bills of materials (SBOMs) promise to become the backbone of software supply chain hardening. We deep-dive into six tools and the SBOMs they produce for complex open source Java projects, revealing challenges regarding the accurate production and usage of SBOMs.
|
|
| 10. |
- Balliu, Musard, et al.
(författare)
-
ENCOVER : Symbolic Exploration for Information Flow Security
- 2012
-
Ingår i: 2012 IEEE 25th Computer Security Foundations Symposium (CSF). - : IEEE. - 9780769547183 ; , s. 30-44
-
Konferensbidrag (refereegranskat)abstract
- We address the problem of program verification for information flow policies by means of symbolic execution and model checking. Noninterference-like security policies are formalized using epistemic logic. We show how the policies can be accurately verified using a combination of concolic testing and SMT solving. As we demonstrate, many scenarios considered tricky in the literature can be solved precisely using the proposed approach. This is confirmed by experiments performed with ENCOVER, a tool based on Java PathFinder and Z3, which we have developed for epistemic noninterference concolic verification.
|
|
