An official website of the United States government
Gradually typed programming languages permit the incremental addition of static types to untyped programs. To remain sound, languages insert run-time checks at the boundaries between typed and untyped code. Unfortunately, performance studies have shown that the overhead of these checks can be disastrously high, calling into question the viability of sound gradual typing. In this paper, we show that by building on existing work on soft contract verification, we can reduce or eliminate this overhead. Our key insight is that while untyped code cannot be trusted by a gradual type system, there is no need to consider only the worst case when optimizing a gradually typed program. Instead, we statically analyze the untyped portions of a gradually typed program to prove that almost all of the dynamic checks implied by gradual type boundaries cannot fail, and can be eliminated at compile time. Our analysis is modular, and can be applied to any portion of a program. We evaluate this approach on a dozen existing gradually typed programs previously shown to have prohibitive performance overhead—with a median overhead of 2.5× and up to 80.6× in the worst case—and eliminate all overhead in most cases, suffering only 1.5× overhead in the worst case.
more »
« less
Iodine: Fast Dynamic Taint Tracking Using Rollback-free Optimistic Hybrid Analysis
Dynamic information-flow tracking (DIFT) is useful for enforcing security policies, but rarely used in practice, as it can slow down a program by an order of magnitude. Static program analyses can be used to prove safe execution states and elide unnecessary DIFT monitors, but the performance improvement from these analyses is limited by their need to maintain soundness. In this paper, we present a novel optimistic hybrid analysis (OHA) to significantly reduce DIFT overhead while still guaranteeing sound results. It consists of a predicated whole-program static taint analysis, which assumes likely invariants gathered from profiles to dramatically improve precision. The optimized DIFT is sound for executions in which those invariants hold true, and recovers to a conservative DIFT for executions in which those invariants are false. We show how to overcome the main problem with using OHA to optimize live executions, which is the possibility of unbounded rollbacks. We eliminate the need for any rollback during recovery by tailoring our predicated static analysis to eliminate only safe elisions of noop monitors. Our tool, Iodine, reduces the overhead of DIFT for enforcing security policies to 9%, which is 4.4x lower than that with traditional hybrid analysis, while still being able to be run on live systems.
more »
« less
- Award ID(s):
- 1703931
- PAR ID:
- 10113845
- Date Published:
- Journal Name:
- IEEE Symposium on Security and Privacy
- Volume:
- 1
- Page Range / eLocation ID:
- 711-725
- Format(s):
- Medium: X
- Sponsoring Org:
- National Science Foundation
More Like this
-
-
Web-based applications are attractive due to their portability. To leverage that, many mobile applications are hybrid, incorporating a web component that implements most of their functionality. While solutions for enforcing security exist for both mobile and web applications, enforcing and reasoning about the security of their combinations is difficult. We argue for a combination of static and dynamic analysis for assurance of end-to-end confidentiality in hybrid apps. We show how information flows in hybrid Android applications can be secured through use of SPARTA, a static analyzer for Android/Java, and JEST, a dynamic monitor for JavaScript, connected by a compatibility layer that translates policies and value representations. This paper reports on our preliminary investigation using a case study.more » « less
-
Aldrich, Jonathan; Salvaneschi, Guido (Ed.)Timing channel attacks are emerging as real-world threats to computer security. In cryptographic systems, an effective countermeasure against timing attacks is the constant-time programming discipline. However, strictly enforcing the discipline manually is both time-consuming and error-prone. While various tools exist for analyzing/verifying constant-time programs, they sacrifice at least one feature among precision, soundness and efficiency. In this paper, we build CtChecker, a sound static analysis for constant-time programming. Under the hood, CtChecker uses a static information flow analysis to identify violations of constant-time discipline. Despite the common wisdom that sound, static information flow analysis lacks precision for real-world applications, we show that by enabling field-sensitivity, context-sensitivity and partial flow-sensitivity, CtChecker reports fewer false positives compared with existing sound tools. Evaluation on real-world cryptographic systems shows that CtChecker analyzes 24K lines of source code in under one minute. Moreover, CtChecker reveals that some repaired code generated by program rewriters supposedly remove timing channels are still not constant-time.more » « less
-
Information flow tracking was proposed more than 40 years ago to address the limitations of access control mechanisms to guarantee the confidentiality and integrity of information flowing within a system, but has not yet been widely applied in practice for security solutions. Here, we survey and systematize literature on dynamic information flow tracking (DIFT) to discover challenges and opportunities to make it practical and effective for security solutions. We focus on common knowledge in the literature and lingering research gaps from two dimensions— (i) the layer of abstraction where DIFT is implemented (software, software/hardware, or hardware) and (ii) the security goal (confidentiality and/or integrity). We observe that two major limitations hinder the practical application of DIFT for on-the-fly security applications: (i) high implementation overhead and (ii) incomplete information flow tracking (low accuracy). We posit, after review of the literature, that addressing these major impedances via hardware parallelism can potentially unleash DIFT’s great potential for systems security, as it can allow security policies to be implemented in a built-in and standardized fashion. Furthermore, we provide recommendations for the next generation of practical and efficient DIFT systems with an eye towards hardware-supported implementations.more » « less
-
Investigating attacks across multiple hosts is challenging. The true dependencies between security-sensitive files, network endpoints, or memory objects from different hosts can be easily concealed by dependency explosion or undefined program behavior (e.g., memory corruption). Dynamic information flow tracking (DIFT) is a potential solution to this problem, but, existing DIFT techniques only track information flow within a single host and lack an efficient mechanism to maintain and synchronize the data flow tags globally across multiple hosts. In this paper, we propose RTAG, an efficient data flow tagging and tracking mechanism that enables practical cross-host attack investigations. RTAG is based on three novel techniques. First, by using a record-and-replay technique, it decouples the dependencies between different data flow tags from the analysis, enabling lazy synchronization between independent and parallel DIFT instances of different hosts. Second, it takes advantage of systemcall-level provenance information to calculate and allocate the optimal tag map in terms of memory consumption. Third, it embeds tag information into network packets to track cross-host data flows with less than 0.05% network bandwidth overhead. Evaluation results show that RTAG is able to recover the true data flows of realistic cross-host attack scenarios. Performance wise, RTAG reduces the memory consumption of DIFT-based analysis by up to 90% and decreases the overall analysis time by 60%-90% compared with previous investigation systems.more » « less
- Free Publicly Accessible Full Text
-
Accepted Manuscript1.0
- Conference Paper:
- https://doi.org/10.1109/SP.2019.00043
