Dynamic taint tracking, a technique that traces relationships between values as a program executes, has been used to support a variety of software engineering tasks. Some taint tracking systems only consider data flows and ignore control flows. As a result, relationships between some values are not reflected by the analysis. Many applications of taint tracking either benefit from or rely on these relationships being traced, but past works have found that tracking control flows resulted in over-tainting, dramatically reducing the precision of the taint tracking system. In this article, we introduce Conflux , alternative semantics for propagating taint tags along control flows. Conflux aims to reduce over-tainting by decreasing the scope of control flows and providing a heuristic for reducing loop-related over-tainting. We created a Java implementation of Conflux and performed a case study exploring the effect of Conflux on a concrete application of taint tracking, automated debugging. In addition to this case study, we evaluated Conflux ’s accuracy using a novel benchmark consisting of popular, real-world programs. We compared Conflux against existing taint propagation policies, including a state-of-the-art approach for reducing control-flow-related over-tainting, finding that Conflux had the highest F1 score on 43 out of the 48 total tests.
more »
« less
Compositional Information Flow Monitoring for Reactive Programs
To prevent applications from leaking users' private data to attackers, researchers have developed runtime information flow control (IFC) mechanisms. Most existing approaches are either based on taint tracking or multi-execution, and the same technique is used to protect the entire application. However, today's applications are typically composed of multiple components from heterogenous and unequally trusted sources. The goal of this paper is to develop a framework to enable the flexible composition of IFC enforcement mechanisms. More concretely, we focus on reactive programs, which is an abstract model for event-driven programs including web and mobile applications. We formalize the semantics of existing IFC enforcement mechanisms with well-defined interfaces for composition, define knowledge-based security guarantees that can precisely quantify the effect of implicit leaks from taint tracking, and prove sound all composed systems that we instantiate the framework with. We identify requirements for future enforcement mechanisms to be securely composed in our framework. Finally, we implement a prototype in OCaml and compare the effects of different compositions.
more »
« less
- Award ID(s):
- 1704542
- NSF-PAR ID:
- 10385222
- Date Published:
- Journal Name:
- 2022 IEEE 7th European Symposium on Security and Privacy (EuroS&P)
- Page Range / eLocation ID:
- 467 to 486
- Format(s):
- Medium: X
- Sponsoring Org:
- National Science Foundation
More Like this
-
-
We present STORM, a web framework that allows developers to build MVC applications with compile-time enforcement of centrally specified data-dependent security policies. STORM ensures security using a Security Typed ORM that refines the (type) abstractions of each layer of the MVC API with logical assertions that describe the data produced and consumed by the underlying operation and the users allowed access to that data. To evaluate the security guarantees of STORM, we build a formally verified reference implementation using the Labeled IO (LIO) IFC framework. We present case studies and end-to- end applications that show how STORM lets developers specify diverse policies while centralizing the trusted code to under 1% of the application, and statically enforces security with modest type annotation overhead, and no run-time cost.more » « less
-
Hardware enclaves are designed to execute small pieces of sensitive code or to operate on sensitive data, in isolation from larger, less trusted systems. Partitioning a large, legacy application requires significant effort. Partitioning an application written in a managed language, such as Java, is more challenging because of mutable language characteristics, extensive code reachability in class libraries, and the inevitability of using a heavyweight runtime. Civet is a framework for partitioning Java applications into enclaves. Civet reduces the number of lines of code in the enclave and uses language-level defenses, including deep type checks and dynamic taint-tracking, to harden the enclave interface. Civet also contributes a partitioned Java runtime design, including a garbage collection design optimized for the peculiarities of enclaves. Civet is efficient for data-intensive workloads; partitioning a Hadoop mapper reduces the enclave overhead from 10 to 16–22% without taint-tracking or 70–80% with taint-tracking.more » « less
-
more » « less
An interleaved-Dyck (InterDyck) language consists of the interleaving of two or more Dyck languages, where each Dyck language represents a set of strings of balanced parentheses.InterDyck-reachability is a fundamental framework for program analyzers that simultaneously track multiple properly-matched pairs of actions such as call/return, lock/unlock, or write-data/read-data.Existing InterDyck-reachability algorithms are based on the well-known tabulation technique.
This paper presents a new perspective on solving InterDyck-reachability. Our key observation is that for the single-source-single-target InterDyck-reachability variant, it is feasible to summarize all paths from the source node to the target node based on
path expressions . Therefore, InterDyck-reachability becomes an InterDyck-path-recognition problem over path expressions. Instead of computing summary edges as in traditional tabulation algorithms, this new perspective enables us to express InterDyck-reachability as aparenthesis-counting problem, which can be naturally formulated via integer linear programming (ILP).We implemented our ILP-based algorithm and performed extensive evaluations based on two client analyses (a reachability analysis for concurrent programs and a taint analysis). In particular, we evaluated our algorithm against two types of algorithms: (1) the general all-pairs InterDyck-reachability algorithms based on linear conjunctive language (LCL) reachability and synchronized pushdown system (SPDS) reachability, and (2) two domain-specific algorithms for both client analyses. The experimental results are encouraging. Our algorithm achieves 1.42×, 28.24×, and 11.76× speedup for the concurrency-analysis benchmarks compared to all-pair LCL-reachability, SPDS-reachability, and domain-specific tools, respectively; 1.2×, 69.9×, and 0.98× speedup for the taint-analysis benchmarks. Moreover, the algorithm also provides precision improvements, particularly for taint analysis, where it achieves 4.55%, 11.1%, and 6.8% improvement, respectively.
-
more » « less
Policy Points Suboptimal intake of fruit and vegetables is associated with increased risk of diet‐related diseases. A national retail‐based fruit and vegetable subsidy program could broadly benefit the health of the entire population.
Existing fruit and vegetable subsidy programs can inform potential implementation mechanisms; Congress's powers to tax, spend, and regulate interstate commerce can be leveraged to create a federal program.
Legal and administrative feasibility considerations support a conditional funding program or a federal‐state cooperative program combining regulation, licensing, and state or local options for flexible implementation strategies. Strategies to engage key stakeholders would enable the program to utilize lessons learned from existing programs.
Context Suboptimal intake of fruit and vegetables (F&Vs) is associated with increased risk of diet‐related diseases. Yet, there are no US government programs to support increased F&V consumption nationally for the whole population, most of whom purchase food at retail establishments. To inform policy discussion and implementation, we identified mechanisms to effectuate a national retail‐based F&V subsidy program.
Methods We conducted legal and policy research using LexisNexis, the UConn Rudd Center Legislation Database, the Centers for Disease Control and Prevention Chronic Disease State Policy Tracking System, the US Department of Agriculture's website, Congress.gov, gray literature, and government reports. First, we identified existing federal, state, local, and nongovernmental organization (NGO) policies and programs that subsidize F&Vs. Second, we evaluated Congress's power to implement a national retail‐based F&V subsidy program.
Findings We found five federal programs, three federal bills, four state laws, and 17 state (including the District of Columbia [DC]) bills to appropriate money to supplement federal food assistance programs with F&Vs; 74 programs (six multistate, 22 state [including DC], and 46 local) administered by state and local governments and NGOs that incentivize the purchase of F&Vs for various subpopulations; and two state laws and 11 state bills to provide tax exemptions for F&Vs. To create a national F&V subsidy program, Congress could use its Commerce Clause powers or its powers to tax or spend, through direct regulation, licensing, taxation, tax incentives, and conditional funding. Legal and administrative feasibility considerations support a voluntary conditional funding program or, as a second option, a mandatory federal‐state cooperative program combining regulation and licensing.
Conclusions Multiple existing programs provide an important foundation to inform potential implementation mechanisms for a national F&V subsidy program. Results also highlight the value of state and local participation to leverage existing networks and stakeholder knowledge.
- Free Publicly Accessible Full Text
-
Accepted Manuscript1.0
- Conference Paper:
- https://doi.org/10.1109/EuroSP53844.2022.00036
