kth.sePublications
Change search
Refine search result
1 - 29 of 29
CiteExportLink to result list
Permanent link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Rows per page
  • 5
  • 10
  • 20
  • 50
  • 100
  • 250
Sort
  • Standard (Relevance)
  • Author A-Ö
  • Author Ö-A
  • Title A-Ö
  • Title Ö-A
  • Publication type A-Ö
  • Publication type Ö-A
  • Issued (Oldest first)
  • Issued (Newest first)
  • Created (Oldest first)
  • Created (Newest first)
  • Last updated (Oldest first)
  • Last updated (Newest first)
  • Disputation date (earliest first)
  • Disputation date (latest first)
  • Standard (Relevance)
  • Author A-Ö
  • Author Ö-A
  • Title A-Ö
  • Title Ö-A
  • Publication type A-Ö
  • Publication type Ö-A
  • Issued (Oldest first)
  • Issued (Newest first)
  • Created (Oldest first)
  • Created (Newest first)
  • Last updated (Oldest first)
  • Last updated (Newest first)
  • Disputation date (earliest first)
  • Disputation date (latest first)
Select
The maximal number of hits you can export is 250. When you want to export more records please use the Create feeds function.
  • 1.
    Ahmadian, Amir M.
    et al.
    KTH, School of Electrical Engineering and Computer Science (EECS), Computer Science, Theoretical Computer Science, TCS.
    Balliu, Musard
    KTH, School of Electrical Engineering and Computer Science (EECS), Computer Science, Theoretical Computer Science, TCS.
    Dynamic Policies Revisited2022In: Proceedings - 7th IEEE European Symposium on Security and Privacy, Euro S and P 2022, Institute of Electrical and Electronics Engineers (IEEE), 2022, p. 448-466Conference paper (Refereed)
    Abstract [en]

    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.

    Download full text (pdf)
    fulltext
  • 2. Ahmadpanah, M. M.
    et al.
    Balliu, Musard
    KTH, School of Electrical Engineering and Computer Science (EECS), Computer Science, Theoretical Computer Science, TCS.
    Hedin, D.
    Olsson, L. E.
    Sabelfeld, A.
    Securing Node-RED Applications2021In: Protocols, Strands, and LogicEssays Dedicated to Joshua Guttman on the Occasion of his 66.66th Birthday, Springer Science and Business Media Deutschland GmbH , 2021, p. 1-21Conference paper (Refereed)
    Abstract [en]

    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.

  • 3.
    Ahmadpanah, Mohammad M.
    et al.
    Chalmers.
    Hedin, Daniel
    Chalmers and Mälardalen University.
    Balliu, Musard
    KTH, School of Electrical Engineering and Computer Science (EECS), Computer Science, Theoretical Computer Science, TCS.
    Olsson, Lars Eric
    Chalmers.
    Sabelfeld, Andrei
    Chalmers.
    SandTrap: Securing JavaScript-driven Trigger-Action Platforms2021Conference paper (Refereed)
    Download full text (pdf)
    fulltext
  • 4.
    Ahmadpanah, Mohammad M.
    et al.
    Chalmers Univ Technol, Gothenburg, Sweden..
    Hedin, Daniel
    Chalmers Univ Technol, Gothenburg, Sweden.;Mälardalen Univ, Västerås, Sweden..
    Balliu, Musard
    KTH, School of Electrical Engineering and Computer Science (EECS), Computer Science, Theoretical Computer Science, TCS.
    Olsson, Lars Eric
    Chalmers Univ Technol, Gothenburg, Sweden..
    Sabelfeld, Andrei
    Chalmers Univ Technol, Gothenburg, Sweden..
    SandTrap: Securing JavaScript-driven Trigger-Action Platforms2021In: Proceedings Of The 30Th USENIX Security Symposium, USENIX ASSOC , 2021, p. 2899-2916Conference paper (Refereed)
    Abstract [en]

    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.

  • 5.
    Balliu, Musard
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    A Logic for Information Flow Analysis of Distributed Programs2013In: Secure IT Systems: 18th Nordic Conference, NordSec 2013 Ilulissat, Greenland, October 2013 Proceedings, Springer Berlin/Heidelberg, 2013, p. 84-99Conference paper (Refereed)
    Abstract [en]

    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.

    Download full text (pdf)
    fulltext
  • 6.
    Balliu, Musard
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    A Logic for Information Flow Analysis of Distributed Programs: (Extended Abstract)2013Report (Other academic)
    Abstract [en]

    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.

    Download full text (pdf)
    NordSec13_extended
  • 7.
    Balliu, Musard
    et al.
    KTH, School of Electrical Engineering and Computer Science (EECS), Computer Science, Theoretical Computer Science, TCS.
    Bastys, Iulia
    Chalmers Univ Technol, Dept Comp Sci & Engn, Gothenburg, Sweden..
    Sabelfeld, Andrei
    Chalmers Univ Technol, Dept Comp Sci & Engn, Gothenburg, Sweden..
    Securing IoT Apps2019In: IEEE Security and Privacy, ISSN 1540-7993, E-ISSN 1558-4046, Vol. 17, no 5, p. 22-29Article in journal (Refereed)
    Abstract [en]

    Users increasingly rely on Internet of Things (IoT) apps to manage their digital lives through the overwhelming diversity of IoT services and devices. Are the IoT app platforms doing enough to protect the privacy and security of their users? By securing IoT apps, how can we help users reclaim control over their data?

    Download full text (pdf)
    fulltext
  • 8.
    Balliu, Musard
    et al.
    KTH, School of Electrical Engineering and Computer Science (EECS), Computer Science, Theoretical Computer Science, TCS.
    Baudry, Benoit
    KTH, School of Electrical Engineering and Computer Science (EECS), Computer Science, Software and Computer systems, SCS.
    Bobadilla, Sofia
    KTH, School of Electrical Engineering and Computer Science (EECS), Computer Science, Theoretical Computer Science, TCS.
    Ekstedt, Mathias
    KTH, School of Electrical Engineering and Computer Science (EECS), Computer Science, Network and Systems Engineering.
    Monperrus, Martin
    KTH, School of Electrical Engineering and Computer Science (EECS), Computer Science, Theoretical Computer Science, TCS.
    Ron Arteaga, Javier
    KTH, School of Electrical Engineering and Computer Science (EECS), Computer Science, Theoretical Computer Science, TCS.
    Sharma, Aman
    KTH, School of Electrical Engineering and Computer Science (EECS), Computer Science, Theoretical Computer Science, TCS.
    Skoglund, Gabriel
    KTH, School of Electrical Engineering and Computer Science (EECS), Computer Science, Theoretical Computer Science, TCS.
    Soto Valero, César
    KTH, School of Electrical Engineering and Computer Science (EECS), Computer Science, Software and Computer systems, SCS.
    Wittlinger, Martin
    KTH, School of Electrical Engineering and Computer Science (EECS), Computer Science, Theoretical Computer Science, TCS.
    Challenges of Producing Software Bill of Materials for Java2023In: IEEE Security and Privacy, ISSN 1540-7993, E-ISSN 1558-4046, Vol. 21, no 6, p. 12-23Article in journal (Refereed)
    Abstract [en]

    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.

  • 9.
    Balliu, Musard
    et al.
    KTH, School of Electrical Engineering and Computer Science (EECS), Computer Science, Theoretical Computer Science, TCS.
    Baudry, Benoit
    KTH, School of Electrical Engineering and Computer Science (EECS), Computer Science, Software and Computer systems, SCS.
    Bobadilla, Sofia
    KTH, School of Electrical Engineering and Computer Science (EECS), Computer Science, Theoretical Computer Science, TCS.
    Ekstedt, Mathias
    KTH, School of Electrical Engineering and Computer Science (EECS), Computer Science, Network and Systems Engineering.
    Monperrus, Martin
    KTH, School of Electrical Engineering and Computer Science (EECS), Computer Science, Theoretical Computer Science, TCS.
    Ron Arteaga, Javier
    KTH, School of Electrical Engineering and Computer Science (EECS), Computer Science, Theoretical Computer Science, TCS.
    Sharma, Aman
    KTH, School of Electrical Engineering and Computer Science (EECS), Computer Science, Theoretical Computer Science, TCS.
    Skoglund, Gabriel
    KTH, School of Electrical Engineering and Computer Science (EECS), Computer Science, Theoretical Computer Science, TCS.
    Soto Valero, César
    KTH, School of Electrical Engineering and Computer Science (EECS), Computer Science, Software and Computer systems, SCS.
    Wittlinger, Martin
    KTH, School of Electrical Engineering and Computer Science (EECS), Computer Science, Theoretical Computer Science, TCS.
    Software Bill of Materials in Java2023In: SCORED 2023 - Proceedings of the 2023 Workshop on Software Supply Chain Offensive Research and Ecosystem Defenses, Association for Computing Machinery (ACM) , 2023, p. 75-76Conference paper (Refereed)
    Abstract [en]

    Modern software applications are virtually never built entirely in-house. As a matter of fact, they reuse many third-party dependencies, which form the core of their software supply chain [1]. The large number of dependencies in an application has turned into a major challenge for both security and reliability. For example, to compromise a high-value application, malicious actors can choose to attack a less well-guarded dependency of the project [2]. Even when there is no malicious intent, bugs can propagate through the software supply chain and cause breakages in applications. Gathering accurate, upto- date information about all dependencies included in an application is, therefore, of vital importance.

  • 10.
    Balliu, Musard
    et al.
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Dam, Mads
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Guanciale, Roberto
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Automating Information Flow Analysis of Low Level Code2014In: Proceedings of CCS’14, November 3–7, 2014, Scottsdale, Arizona, USA, Association for Computing Machinery (ACM), 2014Conference paper (Refereed)
    Abstract [en]

    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.

    Download full text (pdf)
    ccs14_bdg
  • 11.
    Balliu, Musard
    et al.
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Dam, Mads
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Le Guernic, Gurvan
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    ENCOVER: Symbolic Exploration for Information Flow Security2012In: 2012 IEEE 25th Computer Security Foundations Symposium (CSF), IEEE , 2012, p. 30-44Conference paper (Refereed)
    Abstract [en]

    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.

  • 12.
    Balliu, Musard
    et al.
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Dam, Mads
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Le Guernic, Gurvan
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Epistemic Temporal Logic for Information Flow Security2011In: In proc. of th 4e ACM SIGPLAN workshop on Programming Languages and Analysis for Security, 2011Conference paper (Refereed)
    Abstract [en]

    Temporal epistemic logic is a well-established framework for expressing agents knowledge and how it evolves over time. Within language-based security these are central issues, for instance in the context of declassification. We propose to bring these two areas together. The paper presents a computational model and an epistemic temporal logic used to reason about knowledge acquired by observing program outputs. This approach is shown to elegantly capture standard notions of noninterference and declassification in the literature as well as information flow properties where sensitive and public data intermingle in delicate ways.

  • 13.
    Balliu, Musard
    et al.
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Mastroeni, Isabella
    A Weakest Precondition Approach to Robustness2010In: Lecture Notes in Computer Science, ISSN 0302-9743, E-ISSN 1611-3349, Vol. 6340, no PART 1, p. 261-297Article in journal (Refereed)
    Abstract [en]

    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.

  • 14.
    Balliu, Musard
    et al.
    KTH, School of Electrical Engineering and Computer Science (EECS), Computer Science, Theoretical Computer Science, TCS.
    Merro, Massimo
    University of Verona.
    Pasqua, Michele
    University of Verona.
    Friendly Fire: Cross-App Interactions in IoT Platforms2020In: https://www.cambridge.org/core/what-we-publish/textbooks#, 2020Conference paper (Refereed)
    Abstract [en]

    IoT platforms enable users to connect various smart devices and online services viareactive apps running on the cloud. These apps, often developed by third-parties, performsimple computations on data triggered by external information sources and actuate theresults of computation on external information sinks. Recent research shows that unin-tended or malicious interactions between the dierent (even benign) apps of a user cancause severe security and safety risks. These works leverage program analysis techniquesto build tools for unveiling unexpected interference across apps for specic use cases.We propose a calculus that models the behavioral semantics of a system of apps ex-ecuting concurrently, and use it to dene desirable semantic policies in the security andsafety context of IoT apps. To demonstrate the usefulness of our framework, we denestatic mechanisms for enforcing cross-app security and safety, and prove them sound withrespect to our semantic conditions. Finally, we leverage real-world apps to validate thepractical benets of our policy framework.

    Download full text (pdf)
    fulltext
  • 15.
    Balliu, Musard
    et al.
    KTH, School of Electrical Engineering and Computer Science (EECS), Computer Science, Theoretical Computer Science, TCS.
    Merro, Massimo
    University of Verona.
    Pasqua, Michele
    University of Verona.
    Securing Cross-App Interactions in IoT Platforms2019In: 2019 IEEE 32nd Computer Security Foundations Symposium (CSF), IEEE Computer Society, 2019, p. 319-334, article id 8823751Conference paper (Refereed)
    Abstract [en]

    IoT platforms enable users to connect various smart devices and online services via reactive apps running on the cloud. These apps, often developed by third-parties, perform simple computations on data triggered by external information sources and actuate the results of computation on external information sinks. Recent research shows that unintended or malicious interactions between the different (even benign) apps of a user can cause severe security and safety risks. These works leverage program analysis techniques to build tools for unveiling unexpected interference across apps for specific use cases. Despite these initial efforts, we are still lacking a semantic framework for understanding interactions between IoT apps. The question of what security policy cross-app interference embodies remains largely unexplored. This paper proposes a semantic framework capturing the essence of cross-app interactions in IoT platforms. The framework generalizes and connects syntactic enforcement mechanisms to bisimulation-based notions of security, thus providing a baseline for formulating soundness criteria of these enforcement mechanisms. Specifically, we present a calculus that models the behavioral semantics of a system of apps executing concurrently, and use it to define desirable semantic policies in the security and safety context of IoT apps. To demonstrate the usefulness of our framework, we define static mechanisms for enforcing crossapp security and safety, and prove them sound with respect to our semantic conditions. Finally, we leverage real-world apps to validate the practical benefits of our policy framework.

    Download full text (pdf)
    fulltext
  • 16.
    Balliu, Musard
    et al.
    KTH, School of Electrical Engineering and Computer Science (EECS), Computer Science, Theoretical Computer Science, TCS.
    Merro, Massimo
    University of Verona.
    Pasqua, Michele
    University of Verona.
    Shcherbakov, Mikhail
    KTH, School of Electrical Engineering and Computer Science (EECS), Computer Science, Theoretical Computer Science, TCS.
    Friendly Fire: Cross-App Interactions in IoT Platforms2021In: ACM Transactions on Privacy and Security (TOPS), ISSN 2471-2566, Vol. 24, no 3, p. 1-40, article id 16Article in journal (Refereed)
    Abstract [en]

    IoT platforms enable users to connect various smart devices and online services via reactive apps running onthe cloud. These apps, often developed by third-parties, perform simple computations on data triggered byexternal information sources and actuate the results of computations on external information sinks. Recentresearch shows that unintended or malicious interactions between the different (even benign) apps of a usercan cause severe security and safety risks. These works leverage program analysis techniques to build toolsfor unveiling unexpected interference across apps for specific use cases. Despite these initial efforts, we arestill lacking a semantic framework for understanding interactions between IoT apps. The question of whatsecurity policy cross-app interference embodies remains largely unexplored.This paper proposes a semantic framework capturing the essence of cross-app interactions in IoT platforms.The framework generalizes and connects syntactic enforcement mechanisms to bisimulation-based notionsof security, thus providing a baseline for formulating soundness criteria of these enforcement mechanisms.Specifically, we present a calculus that models the behavioral semantics of a system of apps executingconcurrently, and use it to define desirable semantic policies targeting the security and safety of IoT apps.To demonstrate the usefulness of our framework, we define and implement static analyses for enforcingcross-app security and safety, and prove them sound with respect to our semantic conditions. We also leveragereal-world apps to validate the practical benefits of our tools based on the proposed enforcement mechanisms.

    Download full text (pdf)
    fulltext
  • 17.
    Bastys, Iulia
    et al.
    Chalmers University of Technology.
    Balliu, Musard
    KTH, School of Electrical Engineering and Computer Science (EECS), Computer Science, Theoretical Computer Science, TCS.
    Rezk, Tamara
    INRIA Sophia-Antipolis.
    Sabelfeld, Andrei
    Chalmers University of Technology.
    Clockwork: Tracking Remote Timing Attacks2020In: Proceedings IEEE Computer Security Foundations Symposium, CSF 2020, IEEE , 2020Conference paper (Refereed)
    Abstract [en]

    Timing leaks have been a major concern for the security community. A common approach is to prevent secrets from affecting the execution time, thus achieving security with respect to a strong, local attacker who can measure the timing of program runs. However, this approach becomes restrictive as soon as programs branch on a secret. This paper focuses on timing leaks under remote execution. A key difference is that the remote attacker does not have a reference point of when a program run has started or finished, which significantly restricts attacker capabilities. We propose an extensional security characterization that captures the essence of remote timing attacks. We identify patterns of combining clock access, secret branching, and output in a way that leads to timing leaks. Based on these patterns, we design Clockwork, a monitor that rules out remote timing leaks. We implement the approach for JavaScript, leveraging JSFlow, a state-of-the-art information flow tracker. We demonstrate the feasibility of the approach on case studies with IFTTT, a popular IoT app platform, and VJSC, an advanced JavaScript library for e-voting.

    Download full text (pdf)
    fulltext
  • 18.
    Bastys, Iulia
    et al.
    Chalmers University of Technology.
    Balliu, Musard
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Sabelfeld, Andrei
    Chalmers University of Technology.
    If This Then What? Controlling Flows in IoT Apps2018Conference paper (Refereed)
    Abstract [en]

    IoT apps empower users by connecting a variety of otherwise unconnected services. These apps (or applets) are triggered by external information sources to perform actions on external information sinks. We demonstrate that the popular IoT app platforms, including IFTTT (If This Then That), Zapier, and Microsoft Flow are susceptible to attacks by malicious applet makers, including stealthy privacy attacks to exfiltrate private photos, leak user location, and eavesdrop on user input to voice-controlled assistants. We study a dataset of 279,828 IFTTT applets from more than 400 services, classify the applets according to the sensitivity of their sources, and find that 30% of the applets may violate privacy. We propose two countermeasures for short-and longterm protection: access control and information flow control. For short-term protection, we suggest that access control classifies an applet as either exclusively private or exclusively public, thus breaking flows from private sources to sensitive sinks. For longterm protection, we develop a framework for information flow tracking in IoT apps. The framework models applet reactivity and timing behavior, while at the same time faithfully capturing the subtleties of attacker observations caused by applet output. We show how to implement the approach for an IFTTT-inspired setting leveraging state-of-the-art information flow tracking techniques for JavaScript based on the JSFlow tool and evaluate its effectiveness on a collection of applets.

    Download full text (pdf)
    ccs18
  • 19.
    Birgersson, Marcus
    et al.
    KTH, School of Electrical Engineering and Computer Science (EECS), Computer Science, Theoretical Computer Science, TCS.
    Artho, Cyrille
    KTH, School of Electrical Engineering and Computer Science (EECS), Computer Science, Theoretical Computer Science, TCS.
    Balliu, Musard
    KTH, School of Electrical Engineering and Computer Science (EECS), Computer Science, Theoretical Computer Science, TCS.
    Security-Aware Multi-User Architecture for IoT2021In: 2021 IEEE 21ST INTERNATIONAL CONFERENCE ON SOFTWARE QUALITY, RELIABILITY AND SECURITY (QRS 2021), Institute of Electrical and Electronics Engineers Inc. , 2021, p. 102-113Conference paper (Refereed)
    Abstract [en]

    IoT systems, such as in smart cities or hospitals, generate data that may be subject to different security classifications, privacy regulations, and access rights. However, popular IoT platforms do not consider data classification and security-aware data analysis. In this paper, we present a novel architecture based on open-source solutions that handles the issue of collecting and classifying data at the source and presents the data analysis to users at different authorization levels. Our architecture consists of three layers: a layer for exposing collected and classified data to a middleware, the middleware to handle storage and analysis of the data and expose it to a dashboard, and the dashboard responsible for authenticating users and visualizing data according to the users' classification level. Our solution distinguishes itself by focusing on data classification rather than data collection, supporting fine-grained access control and declassification. Our implementation, using the Web of Things API, Node-RED and Grafana, demonstrates the security benefits of our design on use cases in the smart city and healthcare domains.

    Download full text (pdf)
    fulltext
  • 20.
    Guanciale, Roberto
    et al.
    KTH, School of Electrical Engineering and Computer Science (EECS), Computer Science, Theoretical Computer Science, TCS.
    Balliu, Musard
    KTH, School of Electrical Engineering and Computer Science (EECS), Computer Science, Theoretical Computer Science, TCS.
    Dam, Mads
    KTH, School of Electrical Engineering and Computer Science (EECS), Computer Science, Theoretical Computer Science, TCS.
    InSpectre: Breaking and Fixing Microarchitectural Vulnerabilities by Formal Analysis2020In: CCS '20: Proceedings of the 2020 ACM SIGSAC Conference on Computer and Communications, Association for Computing Machinery (ACM) , 2020Conference paper (Refereed)
    Abstract [en]

    The recent Spectre attacks have demonstrated the fundamental insecurity of current computer microarchitecture. The attacks use features like pipelining, out-of-order and speculation to extract arbitrary information about the memory contents of a process. A comprehensive formal microarchitectural model capable of representing the forms of out-of-order and speculative behavior that can meaningfully be implemented in a high performance pipelined architecture has not yet emerged. Such a model would be very useful, as it would allow the existence and non-existence of vulnerabilities, and soundness of countermeasures to be formally established. This paper presents such a model targeting single core processors. The model is intentionally very general and provides an infrastructure to define models of real CPUs. It incorporates microarchitectural features that underpin all known Spectre vulnerabilities. We use the model to elucidate the security of existing and new vulnerabilities, as well as to formally analyze the effectiveness of proposed countermeasures. Specifically, we discover three new (potential) vulnerabilities, including a new variant of Spectre v4, a vulnerability on speculative fetching, and a vulnerability on out-of-order execution, and analyze the effectiveness of existing countermeasures including constant time and serializing instructions.  

  • 21.
    Guarnieri, Marco
    et al.
    IMDEA Software Institute.
    Balliu, Musard
    KTH, School of Electrical Engineering and Computer Science (EECS), Computer Science, Theoretical Computer Science, TCS.
    Schoepe, Daniel
    Chalmers University of Technology.
    Basin, David
    ETH Zurich.
    Sabelfeld, Andrei
    Chalmers University of Technology.
    Information-Flow Control for Database-backed Applications2019Conference paper (Refereed)
    Abstract [en]

    Securing database-backed applications requires tracking information across the application program and the database together, since securing each component in isolation may still result in an overall insecure system. Current research extends language-based techniques with models capturing the database’s behavior. This research, however, relies on simplistic database models, which ignore security-relevant features that may leak sensitive information. We propose a novel security monitor for database-backed applications. Our monitor tracks fine-grained dependencies between variables and database tuples by leveraging database theory concepts like disclosure lattices and query determinacy. It also accounts for a realistic database model that supports security-critical  constructs like triggers and dynamic policies. The monitor automatically synthesizes program-level code that replicates the behavior of database features like triggers, thereby tracking information flows inside the database. We also introduce symbolic tuples, an efficient approximation of dependency-tracking over disclosure lattices. We implement our monitor for SCALA programs and demonstrate its effectiveness on four case studies.

    Download full text (pdf)
    fulltext
  • 22.
    Oak, Aditya
    et al.
    TU Darmstadt.
    Ahmadian, Amir M.
    KTH, School of Electrical Engineering and Computer Science (EECS), Computer Science, Theoretical Computer Science, TCS.
    Balliu, Musard
    KTH, School of Electrical Engineering and Computer Science (EECS), Computer Science, Theoretical Computer Science, TCS.
    Salvaneschi, Guido
    University of St.Gallen.
    Enclave-Based Secure Programming with JE2021In: 2021 IEEE SECURE DEVELOPMENT CONFERENCE (SECDEV 2021), Institute of Electrical and Electronics Engineers (IEEE) , 2021Conference paper (Refereed)
    Abstract [en]

    Over the past few years, major hardware vendors have started offering processors that support Trusted Execution Environments (TEEs) allowing confidential computations over sensitive data on untrusted hosts. Unfortunately, developing applications that use TEEs remains challenging. Current solutions require using low-level languages (e.g., C/C++) to handle the TEE management process manually a complex and error-prone task. Worse, the separation of the application into components that run inside and outside the TEE may lead to information leaks. In summary, TEEs are a powerful means to design secure applications, but there is still a long way to building secure software with TEEs alone. In this work, we present J(E), a programming model for developing TEE-enabled applications where developers only need to annotate Java programs to define application-level security policies and run them securely inside enclaves.

    Download full text (pdf)
    fulltext
  • 23.
    Oak, Aditya
    et al.
    TU Darmstadt.
    Ahmadian, Amir M.
    KTH, School of Electrical Engineering and Computer Science (EECS), Computer Science, Theoretical Computer Science, TCS.
    Balliu, Musard
    KTH, School of Electrical Engineering and Computer Science (EECS), Computer Science, Theoretical Computer Science, TCS.
    Salvaneschi, Guido
    University of St.Gallen.
    Language Support for Secure Software Development with Enclaves2021Conference paper (Refereed)
    Download full text (pdf)
    fulltext
  • 24.
    Shcherbakov, Mikhail
    et al.
    KTH, School of Electrical Engineering and Computer Science (EECS), Computer Science, Theoretical Computer Science, TCS.
    Balliu, Musard
    KTH, School of Electrical Engineering and Computer Science (EECS), Computer Science, Theoretical Computer Science, TCS.
    SerialDetector: Principled and Practical Exploration of Object Injection Vulnerabilities for the Web2021In: Proceedings of the Network and Distributed System Security Symposium (NDSS 2021), 2021Conference paper (Refereed)
    Abstract [en]

    The last decade has seen a proliferation of code-reuse attacks in the context of web applications. These at-tacks stem from Object Injection Vulnerabilities (OIV) enablingattacker-controlled data to abuse legitimate code fragmentswithin a web application’s codebase to execute a code chain(gadget) that performs malicious computations, like remote codeexecution, on attacker’s behalf. OIVs occur when untrusted datais used to instantiate an object of attacker-controlled type withattacker-chosen properties, thus triggering the execution of codeavailable but not necessarily used by the application. In theweb application domain, OIVs may arise during the processof deserialization of client-side data, e.g., HTTP requests, whenreconstructing the object graph that is subsequently processedby the backend applications on the server side.This paper presents the first systematic approach for de-tecting and exploiting OIVs in .NET applications including theframework and libraries. Our key insight is: The root cause ofOIVs is the untrusted information flow from an application’spublic entry points (e.g., HTTP request handlers) to sensitivemethods that create objects of arbitrary types (e.g., reflectionAPIs) to invoke methods (e.g., native/virtual methods) that triggerthe execution of a gadget. Drawing on this insight, we developand implement SerialDetector, a taint-based dataflow analysisthat discovers OIV patterns in .NET assemblies automatically.We then use these patterns to match publicly available gadgetsand to automatically validate the feasibility of OIV attacks.We demonstrate the effectiveness of our approach by an in-depth evaluation of a complex production software such as theAzure DevOps Server. We describe the key threat models andreport on several remote code execution vulnerabilities found bySerialDetector, including three CVEs on Azure DevOps Server.We also perform an in-breadth security analysis of recent publiclyavailable CVEs. Our results show that SerialDetector can detectOIVs effectively and efficiently. We release our tool publicly tosupport open science and encourage researchers and practitionersexplore the topic further

    Download full text (pdf)
    fulltext
  • 25.
    Shcherbakov, Mikhail
    et al.
    KTH, School of Electrical Engineering and Computer Science (EECS), Computer Science, Theoretical Computer Science, TCS.
    Balliu, Musard
    KTH, School of Electrical Engineering and Computer Science (EECS), Computer Science, Theoretical Computer Science, TCS.
    Staicu, Cristian-Alexandru
    CISPA Helmholtz Ctr Informat Secur, Saarbrucken, Germany..
    Silent Spring: Prototype Pollution Leads to Remote Code Execution in Node.js2023In: Proceedings Of The 32Nd Usenix Security Symposium, USENIX ASSOC , 2023, p. 5521-5538Conference paper (Refereed)
    Abstract [en]

    Prototype pollution is a dangerous vulnerability affecting prototype-based languages like JavaScript and the Node.js platform. It refers to the ability of an attacker to inject properties into an object's root prototype at runtime and subsequently trigger the execution of legitimate code gadgets that access these properties on the object's prototype, leading to attacks such as Denial of Service (DoS), privilege escalation, and Remote Code Execution (RCE). While there is anecdotal evidence that prototype pollution leads to RCE, current research does not tackle the challenge of gadget detection, thus only showing feasibility of DoS attacks, mainly against Node.js libraries. In this paper, we set out to study the problem in a holistic way, from the detection of prototype pollution to detection of gadgets, with the ambitious goal of finding end-to-end exploits beyond DoS, in full-fledged Node.js applications. We build the first multi-staged framework that uses multilabel static taint analysis to identify prototype pollution in Node.js libraries and applications, as well as a hybrid approach to detect universal gadgets, notably, by analyzing the Node.js source code. We implement our framework on top of GitHub's static analysis framework CodeQL to find 11 universal gadgets in core Node.js APIs, leading to code execution. Furthermore, we use our methodology in a study of 15 popular Node.js applications to identify prototype pollutions and gadgets. We manually exploit eight RCE vulnerabilities in three high-profile applications such as NPM CLI, Parse Server, and Rocket.Chat. Our results provide alarming evidence that prototype pollution in combination with powerful universal gadgets lead to RCE in Node.js.

  • 26.
    Shcherbakov, Mikhail
    et al.
    KTH, School of Electrical Engineering and Computer Science (EECS), Computer Science, Theoretical Computer Science, TCS.
    Moosbrugger, Paul
    KTH, School of Electrical Engineering and Computer Science (EECS).
    Balliu, Musard
    KTH, School of Electrical Engineering and Computer Science (EECS), Computer Science, Theoretical Computer Science, TCS.
    Unveiling the Invisible: Detection and Evaluation of Prototype Pollution Gadgets with Dynamic Taint Analysis2024In: WWW 2024 - Proceedings of the ACM Web Conference, Association for Computing Machinery (ACM) , 2024, p. 1800-1811Conference paper (Refereed)
    Abstract [en]

    Prototype-based languages like JavaScript are susceptible to prototype pollution vulnerabilities, enabling an attacker to inject arbitrary properties into an object's prototype. The attacker can subsequently capitalize on the injected properties by executing otherwise benign pieces of code, so-called gadgets, that perform security-sensitive operations. The success of an attack largely depends on the presence of gadgets, leading to high-profile exploits such as privilege escalation and arbitrary code execution (ACE). This paper proposes Dasty, the first semi-automated pipeline to help developers identify gadgets in their applications' software supply chain. Dasty targets server-side Node.js applications and relies on an enhancement of dynamic taint analysis which we implement with the dynamic AST-level instrumentation. Moreover, Dasty provides support for visualization of code flows with an IDE, thus facilitating the subsequent manual analysis for building proof-of-concept exploits. To illustrate the danger of gadgets, we use Dasty in a study of the most dependent-upon NPM packages to analyze the presence of gadgets leading to ACE. Dasty identifies 1,269 server-side packages, of which 631 have code flows that may reach dangerous sinks. We manually prioritize and verify the candidate flows to build proof-of-concept exploits for 49 NPM packages, including popular packages such as ejs, nodemailer and workerpool. To investigate how Dasty integrates with existing tools to find end-to-end exploits, we conduct an in-depth analysis of a popular data visualization dashboard to find one high-severity CVE-2023-31415 leading to remote code execution.

  • 27.
    Staicu, Cristian-Alexandru
    et al.
    TU Darmstadt.
    Schoepe, Daniel
    Chalmers University of Technology.
    Balliu, Musard
    KTH, School of Electrical Engineering and Computer Science (EECS), Computer Science, Theoretical Computer Science, TCS.
    Pradel, Michael
    TU Darmstadt.
    Sabelfeld, Andrei
    Chalmers University of Technology.
    An Empirical Study of Information Flows in Real-World JavaScript2019In: Proceedings of the 14th ACM SIGSAC Workshop on Programming Languages and Analysis for Security, ACM Digital Library, 2019, p. 45-59Conference paper (Refereed)
    Abstract [en]

    Information flow analysis prevents secret or untrusted data from flowing into public or trusted sinks. Existing mechanisms cover a wide array of options, ranging from lightweight taint analysis to heavyweight information flow control that also considers implicit flows. Dynamic analysis, which is particularly popular for languages such as JavaScript, faces the question whether to invest in analyzing flows caused by not executing a particular branch, so-called hidden implicit flows. This paper addresses the questions how common different kinds of flows are in real-world programs, how important these flows are to enforce security policies, and how costly it is to consider these flows. We address these questions in an empirical study that analyzes 56 real-world JavaScript programs that suffer from various security problems, such as code injection vulnerabilities, denial of service vulnerabilities, memory leaks, and privacy leaks. The study is based on a state-of-the-art dynamic information flow analysis and a formalization of its core. We find that implicit flows are expensive to track in terms of permissiveness, label creep, and runtime overhead. We find a lightweight taint analysis to be sufficient for most of the studied security problems, while for some privacy-related code, observable tracking is sometimes required. In contrast, we do not find any evidence that tracking hidden implicit flows reveals otherwise missed security problems. Our results help security analysts and analysis designers to understand the cost-benefit tradeoffs of information flow analysis and provide empirical evidence that analyzing information flows in a cost-effective way is a relevant problem.

  • 28.
    Tsoupidi, Rodothea Myrsini
    et al.
    KTH, School of Electrical Engineering and Computer Science (EECS), Computer Science, Software and Computer systems, SCS.
    Balliu, Musard
    KTH, School of Electrical Engineering and Computer Science (EECS), Computer Science, Theoretical Computer Science, TCS.
    Baudry, Benoit
    KTH, School of Electrical Engineering and Computer Science (EECS), Computer Science, Software and Computer systems, SCS.
    Vivienne: Relational Verification of Cryptographic Implementations in WebAssembly2021In: Proceedings - 2021 IEEE Secure Development Conference, SecDev 2021, Institute of Electrical and Electronics Engineers (IEEE), 2021, p. 94-102Conference paper (Refereed)
    Abstract [en]

    We investigate the use of relational symbolic execution to counter timing side channels in WebAssembly programs.We design and implement VIVIENNE, an open-source tool toautomatically analyze WebAssembly cryptographic libraries forconstant-time violations. Our approach features various optimizations that leverage the structure of WebAssembly andautomated theorem provers, including support for loops viarelational invariants. We evaluate Vivienne on 57 real-worldcryptographic implementations, including a previously unverifiedimplementation of the HACL* library in WebAssembly. Theresults indicate that Vivienne is a practical solution for constanttime analysis of cryptographic libraries in WebAssembly.

    Download full text (pdf)
    fulltext
  • 29.
    Tuma, Katja
    et al.
    Chalmers | University of Gothenburg.
    Balliu, Musard
    KTH, School of Electrical Engineering and Computer Science (EECS), Computer Science, Theoretical Computer Science, TCS.
    Scandariato, Riccardo
    Chalmers | University of Gothenburg.
    Flaws in Flows: Unveiling Design Flaws via Information Flow Analysis2019In: Proceedings - 2019 IEEE International Conference on Software Architecture, ICSA 2019, IEEE, 2019, p. 191-200, article id 8703905Conference paper (Refereed)
    Abstract [en]

    This paper presents a practical and formal approach to analyze security-centric information flow policies at the level of the design model. Specifically, we focus on data confidentiality and data integrity objectives. In its guiding principles, the approach is meant to be amenable for designers (e.g., software architects) that have very limited or no background in formal models, logics, and the like. To this aim, we provide an intuitive graphical notation, which is based on the familiar Data Flow Diagrams, and which requires as little effort as possible in terms of extra security-centric information the designer has to provide. The result of the analysis algorithm is the early discovery of design flaws in the form of violations of the intended security properties. The approach is implemented as a publicly available plugin for Eclipse and evaluated with four real-world case studies from publicly available literature.

    Download full text (pdf)
    fulltext
1 - 29 of 29
CiteExportLink to result list
Permanent link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf