| 1. |
- Schoepe, Daniel, 1989, et al.
(author)
-
SeLINQ: Tracking information across application-database boundaries
- 2014
-
In: SIGPLAN Notices (ACM Special Interest Group on Programming Languages). - New York, NY, USA : ACM. - 0730-8566. - 9781450328739 ; 49:9, s. 25-38
-
Conference paper (peer-reviewed)abstract
- The root cause for confidentiality and integrity attacks against computing systems is insecure information flow. The complexity of modern systems poses a major challenge to secure end-to-end information flow, ensuring that the insecurity of a single component does not render the entire system insecure. While information flow in a variety of languages and settings has been thoroughly studied in isolation, the problem of tracking information across component boundaries has been largely out of reach of the work so far. This is unsatisfactory because tracking information across component boundaries is necessary for end-to-end security. This paper proposes a framework for uniform tracking of information flow through both the application and the underlying database. Key enabler of the uniform treatment is recent work by Cheney et al., which studies database manipulation via an embedded language-integrated query language (with Microsoft's LINQ on the backend). Because both the host language and the embedded query languages are functional F#-like languages, we are able to leverage information-flow enforcement for functional languages to obtain information-flow control for databases "for free", synergize it with information-flow control for applications and thus guarantee security across application-database boundaries. We develop the formal results in the form of a security type system that includes a treatment of algebraic data types and pattern matching, and establish its soundness. On the practical side, we implement the framework and demonstrate its usefulness in a case study with a realistic movie rental database.
|
|
| 2. |
- 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.
|
|
| 3. |
- 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.
|
|
| 4. |
- Bastys, Iulia, 1986, et al.
(author)
-
Automatic Annotation of Confidential Data in Java Code
- 2022
-
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. ; 13291, s. 146-161
-
Conference paper (peer-reviewed)abstract
- The problem of confidential information leak can be addressed by using automatic tools that take a set of annotated inputs (the source ) and track their flow to public sinks . Unfortunately, manually annotating the code with labels specifying the secret sources is one of the main obstacles in the adoption of such trackers. In this work, we present an approach for the automatic generation of labels for confidential data in Java programs. Our solution is based on a graph-based representation of Java methods: starting from a minimal set of known API calls, it propagates the labels both intra- and inter-procedurally until a fix-point is reached. In our evaluation, we encode our synthesis and propagation algorithm in Datalog and assess the accuracy of our technique on seven previously annotated internal code bases, where we can reconstruct 75% of the preexisting manual annotations. In addition to this single data point, we also perform an assessment using samples from the SecuriBench-micro benchmark, and we provide additional sample programs that demonstrate the capabilities and the limitations of our approach.
|
|
| 5. |
- 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.
|
|
| 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
(author)
-
Flexible and Practical Information-Flow Control
- 2016
-
Licentiate thesis (other academic/artistic)abstract
- As more and more sensitive data is handled by software, itstrustworthiness becomes an increasingly important concern. This thesispresents work on ensuring that information that is processed bycomputing systems is not disclosed to third parties without the user'spermission; i.e. to prevent unwanted flows of information. Since mostapproaches to information-flow control have not seen widespread use inpractice, this work explores flexible policies and enforcementtechniques to guarantee that information is not leaked by a program. Thethesis consists of three parts:The first chapter explores opacity, a security policy for protectingsensitive system properties, motivated by location privacy andprivacy-preserving aggregation scenarios. We present a general,parametric framework for opacity and relate it to noninterference.Moreover, we present two approaches to enforcement: a dynamic monitormaking use of SMT solving, and a blackbox sampling-based approachbased on the random testing tool QuickCheck.The second chapter discusses taint tracking, a popular securitymechanism for tracking data-flow dependencies, which is widely usedfor both high-level languages and machine code. However, the questionof what, exactly, tainting means - what security policy it embodies -remains largely unexplored. We propose explicit secrecy, a genericframework capturing the essence of explicit flows, i.e., the dataflows tracked by tainting. We illustrate our approach by instantiatingexplicit secrecy to both, a high-level imperative language and machinecode. Additionally, we prove soundness with respect to explicitsecrecy for the cores of dynamic and static taint trackers.Lastly, we present JSLINQ, a framework providing end-to-endinformation-flow control for multi-tiered web applications; i.e. webapplications consisting of a database, server-side code, andclient-side JavaScript code. To prevent information flows at componentboundaries, we leverage homogeneous meta-programming features in F#to provide a unified language for programming all components. Wepresent a security type system for a core of F# and prove that allwell-typed programs are noninterfering. We evaluate our approach usingvarious case studies indicating that JSLINQ is suitable forimplementing practical web applications.
|
|
| 8. |
- Schoepe, Daniel, 1989
(author)
-
Flexible Information-Flow Control
- 2018
-
Doctoral thesis (other academic/artistic)abstract
- As more and more sensitive data is handled by software, its trustworthiness becomes an increasingly important concern. This thesis presents work on ensuring that information processed by computing systems is not disclosed to third parties without the user's permission; i.e. to prevent unwanted flows of information. While this problem is widely studied, proposed rigorous information-flow control approaches that enforce strong security properties like noninterference have yet to see widespread practical use. Conversely, lightweight techniques such as taint tracking are more prevalent in practice, but lack formal underpinnings, making it unclear what guarantees they provide. This thesis aims to shrink the gap between heavyweight information-flow control approaches that have been proven sound and lightweight practical techniques without formal guarantees such as taint tracking. This thesis attempts to reconcile these areas by (a) providing formal foundations to taint tracking approaches, (b) extending information-flow control techniques to more realistic languages and settings, and (c) exploring security policies and mechanisms that fall in between information-flow control and taint tracking and investigating what trade-offs they incur.
|
|
| 9. |
- 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.
|
|
| 10. |
- Schoepe, Daniel, 1989, et al.
(author)
-
Understanding and Enforcing Opacity
- 2015
-
In: Proceedings. The Computer Security Foundations Workshop III. - 1063-6900. - 9781467375382 ; 2015-September, s. 539-553
-
Conference paper (peer-reviewed)abstract
- This paper puts a spotlight on the specification and enforcement of opacity, a security policy for protecting sensitive properties of system behavior. We illustrate the fine granularity of the opacity policy by location privacy and privacy-preserving aggregation scenarios. We present a framework for opacity and explore its key differences and formal connections with such well-known information-flow models as noninterference, knowledge-based security, and declassification. Our results are machine-checked and parameterized in the observational power of the attacker, including progress-insensitive, progress-sensitive, and timing-sensitive attackers. We present two approaches to enforcing opacity: a whitebox monitor and a blackbox sampling-based enforcement. We report on experiments with prototypes that utilize state-of-the-art Satisfiability Modulo Theories (SMT) solvers and the random testing tool QuickCheck to establish opacity for the location and aggregation-based scenarios.
|
|
| 11. |
- Schoepe, Daniel, 1989, et al.
(author)
-
VERONICA: Expressive and Precise Concurrent Information Flow Security
- 2020
-
In: Proceedings - IEEE Computer Security Foundations Symposium. - 1940-1434. ; 2020-June, s. 79-94
-
Conference paper (peer-reviewed)abstract
- Methods for proving that concurrent software does not leak its secrets has remained an active topic of research for at least the past four decades. Despite an impressive array of work, the present situation remains highly unsatisfactory. With contemporary compositional proof methods one is forced to choose between expressiveness (the ability to reason about a wide variety of security policies), on the one hand, and precision (the ability to reason about complex thread interactions and program behaviours), on the other. Achieving both is essential and, we argue, requires a new style of compositional reasoning.We present VERONICA, the first program logic for proving concurrent programs information flow secure that supports compositional, high-precision reasoning about a wide range of security policies and program behaviours (e.g. expressive declassification, value-dependent classification, secret-dependent branching). Just as importantly, VERONICA embodies a new approach for engineering such logics that can be re-used elsewhere, called decoupled functional correctness (DFC). DFC leads to a simple and clean logic, even while achieving this unprecedented combination of features. We demonstrate the virtues and versatility of VERONICA by verifying a range of example programs, beyond the reach of prior methods.
|
|
| 12. |
- 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.
|
|
