| 1. |
- Balliu, Musard, 1985, et al.
(author)
-
JSLINQ: Building secure applications across tiers
- 2016
-
In: 6th ACM Conference on Data and Application Security and Privacy, CODASPY 2016; New Orleans; United States; 9 March 2016 through 11 March 2016. - New York, NY, USA : ACM. ; , s. 307-318
-
Conference paper (peer-reviewed)abstract
- Modern web and mobile applications are complex entities amalgamating different languages, components, and platforms. The rich features span the application tiers and components, some from third parties, and require substantial efforts to ensure that the insecurity of a single component does not render the entire system insecure. As of today, the majority of the known approaches fall short of ensuring security across tiers. This paper proposes a framework for end-to-end security, by tracking information flow through the client, server, and underlying database. The framework utilizes homogeneous meta-programming to provide a uniform language for programming different components. We leverage. NET metaprogramming capabilities from the F# language, thus enabling language-integrated queries on databases and interoperable heterogeneous execution on the client and the server. We develop a core of our security enforcement in the form of a security type system for a functional language with mutable store and prove it sound. Based on the core, we develop JSLINQ, an extension of the WebSharper library to track information flow. We demonstrate the capabilities of JSLINQ on the case studies of a password meter, two location-based services, a movie rental database, an online Battleship game, and a friend finder app. Our experiments indicate that JSLINQ is practical for implementing high-assurance web and mobile applications.
|
|
| 2. |
- Balliu, Musard, 1985, et al.
(author)
-
We are family: Relating information-flow trackers
- 2017
-
In: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - Cham : Springer International Publishing. - 1611-3349 .- 0302-9743. - 9783319664019 ; 10492 LNCS, s. 124-145
-
Conference paper (peer-reviewed)abstract
- While information-flow security is a well-established area, there is an unsettling gap between heavyweight information-flow control, with formal guarantees yet limited practical impact, and lightweight tainting techniques, useful for bug finding yet lacking formal assurance. This paper proposes a framework for exploring the middle ground in the range of enforcement from tainting (tracking data flows only) to fully-fledged information-flow control (tracking both data and control flows). We formally illustrate the trade-offs between the soundness and permissiveness that the framework allows to achieve. The framework is deployed in a staged fashion, statically embedding a dynamic monitor, being parametric in security policies, as they do not need to be fixed until the final deployment. This flexibility facilitates a secure app store architecture, where the static stage of verification is performed by the app store and the dynamic stage is deployed on the client. To illustrate the practicality of the framework, we implement our approach for a core of Java and evaluate it on a use case with enforcing privacy policies in the Android setting. We also show how a state-of-the-art dynamic monitor for JavaScript can be easily adapted to implement our approach. © 2017, Springer International Publishing AG.
|
|
| 3. |
- Bastys, Iulia, 1986, et al.
(author)
-
Clockwork: Tracking Remote Timing Attacks
- 2020
-
In: Proceedings - IEEE Computer Security Foundations Symposium. - : IEEE. - 1940-1434. ; 2020-June, s. 350-365
-
Conference paper (peer-reviewed)abstract
- 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.
|
|
| 4. |
- Guarnieri, Marco, et al.
(author)
-
Information-flow control for database-backed applications
- 2019
-
In: Proceedings - 4th IEEE European Symposium on Security and Privacy, EURO S and P 2019. - : Institute of Electrical and Electronics Engineers (IEEE). ; June 2019, s. 79-94
-
Conference paper (peer-reviewed)abstract
- 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.
|
|
| 5. |
- Pardo Jimenez, Raul, 1988, et al.
(author)
-
Formalising privacy policies in social networks
- 2017
-
In: Journal of Logical and Algebraic Methods in Programming. - : Elsevier BV. - 2352-2208 .- 2352-2216. ; 90, s. 125-157
-
Journal article (peer-reviewed)abstract
- Social Network Services (SNS) have changed the way people communicate, bringing many benefits but also new concerns. Privacy is one of them. We present a framework to write privacy policies for SNSs and to reason about such policies in the presence of events making the network evolve. The framework includes a model of SNSs, a logic to specify properties and to reason about the knowledge of the users (agents) of the SNS, and a formal language to write privacy policies. Agents are enhanced with a reasoning engine allowing the inference of knowledge from previously acquired knowledge. To describe the way SNSs may evolve, we provide operational semantics rules which are classified into four categories: epistemic, topological, policy, and hybrid, depending on whether the events under consideration change the knowledge of the SNS' users, the structure of the social graph, the privacy policies, or a combination of the above, respectively. We provide specific rules for describing Twitter's behaviour, and prove that it is privacy-preserving (i.e., that privacy is preserved under every possible event of the system). We also show how Twitter and Facebook are not privacy-preserving in the presence of additional natural privacy policies. (C) 2017 Elsevier Inc. All rights reserved.
|
|
| 6. |
- Schoepe, Daniel, 1989, et al.
(author)
-
Explicit Secrecy: A Policy for Taint Tracking
- 2016
-
In: 1st IEEE European Symposium on Security and Privacy (Euro S&P), Saarbruecken, Germany, Mar 21-24, 2016. - 9781509017522 ; , s. 15-30
-
Conference paper (peer-reviewed)abstract
- Taint tracking is a popular security mechanism for tracking data-flow dependencies, both in high-level languages and at the machine code level. But despite the many taint trackers in practical use, the question of what, exactly, tainting means-what security policy it embodies-remains largely unexplored. We propose explicit secrecy, a generic framework capturing the essence of explicit flows, i.e., the data flows tracked by tainting. The framework is semantic, generalizing previous syntactic approaches to formulating soundness criteria of tainting. We demonstrate the usefulness of the framework by instantiating it with both a simple high-level imperative language and an idealized RISC machine. To further understanding of what is achieved by taint tracking tools, both dynamic and static, we obtain soundness results with respect to explicit secrecy for the tainting engine cores of a collection of popular dynamic and static taint trackers.
|
|
| 7. |
- Schoepe, Daniel, 1989, et al.
(author)
-
Let’s face it: Faceted values for taint tracking
- 2016
-
In: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - Cham : Springer International Publishing. - 1611-3349 .- 0302-9743. - 9783319457437 ; 9878 LNCS, 2016, s. 561-580
-
Conference paper (peer-reviewed)abstract
- Taint tracking has been successfully deployed in a range of security applications to track data dependencies in hardware and machine-, binary-, and high-level code. Precision of taint tracking is key for its success in practice: being a vulnerability analysis, false positives must be low for the analysis to be practical. This paper presents an approach to taint tracking, which does not involve tracking taints throughout computation. Instead, we include shadow memories in the execution context, so that a single run of a program has the effect of computing on both tainted and untainted data. This mechanism is inspired by the technique of secure multi-execution, while in contrast to the latter it does not require running the entire program multiple times. We present a general framework and establish its soundness with respect to explicit secrecy, a policy for preventing insecure data leaks, and its precision showing that runs of secure programs are never modified. We show that the technique can be used for attack detection with no false positives. To evaluate the mechanism in practice, we implement DroidFace, a source-to-source transform for an intermediate Java-like language and benchmark its precision and performance with respect to representative static and dynamic taint trackers for Android. The results indicate that the performance penalty is tolerable while achieving both soundness and no false positives on the tested benchmarks.
|
|
| 8. |
- Staicu, Cristian Alexandru, et al.
(author)
-
An empirical study of information flows in real-world Javascript
- 2019
-
In: Proceedings of the ACM Conference on Computer and Communications Security. - New York, NY, USA : ACM. - 1543-7221. ; , s. 45-59, s. 45-59
-
Conference paper (peer-reviewed)abstract
- 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.
|
|
