Maybe-tainted data: Theory and a case study
Department
Computer Science
Document Type
Article
Publication Title
Journal of Computer Security
ISSN
1875-8924
Volume
28
Issue
3
DOI
10.3233/JCS-191342
First Page
1
Last Page
41
Publication Date
Spring 1-1-2020
Abstract
Dynamic taint analysis is often used as a defense against low-integrity data in applications with untrusted user interfaces. An important example is defense against XSS and injection attacks in programs with web interfaces. Data sanitization is commonly used in this context, and can be treated as a precondition for endorsement in a dynamic integrity taint analysis. However, sanitization is often incomplete in practice. We develop a model of dynamic integrity taint analysis for Java that addresses imperfect sanitization with an in-depth approach. To avoid false positives, results of sanitization are endorsed for access control (aka prospective security), but are tracked and logged for auditing and accountability (aka retrospective security). We show how this heterogeneous prospective/retrospective mechanism can be specified as a uniform policy, separate from code. We then use this policy to establish correctness conditions for a program rewriting algorithm that instruments code for the analysis. These conditions synergize our previous work on the semantics of audit logging with explicit integrity which is an analogue of noninterference for taint analysis. A technical contribution of our work is the extension of explicit integrity to a high-level functional language setting with structured data, vs. previous systems that only address low level languages with unstructured data. Our approach considers endorsement which is crucial to address sanitization. An implementation of our rewriting algorithm is presented that hardens the OpenMRS medical records software system with in-depth taint analysis, along with an empirical evaluation of the overhead imposed by instrumentation. Our results show that this instrumentation is practical.
Recommended Citation
Amir-Mohammadian, S.,
Skalka, C.,
&
Clark, S.
(2020).
Maybe-tainted data: Theory and a case study.
Journal of Computer Security, 28(3), 1–41.
DOI: 10.3233/JCS-191342
https://scholarlycommons.pacific.edu/soecs-facarticles/106