Type-based Dependency Analysis for JavaScript

TL;DR

This paper presents a formal, sound, and terminating dependency analysis for JavaScript, based on tainting semantics, which can support security-related investigations like data integrity and confidentiality.

Contribution

It introduces a novel formal dependency analysis for JavaScript, with proofs of correctness, soundness, noninterference, and termination.

Findings

Formalization of dependency analysis as tainting semantics

Proof of noninterference property for JavaScript dependency analysis

Guarantee of analysis termination

Abstract

Dependency analysis is a program analysis that determines potential data flow between program points. While it is not a security analysis per se, it is a viable basis for investigating data integrity, for ensuring confidentiality, and for guaranteeing sanitization. A noninterference property can be stated and proved for the dependency analysis. We have designed and implemented a dependency analysis for JavaScript. We formalize this analysis as an abstraction of a tainting semantics. We prove the correctness of the tainting semantics, the soundness of the abstraction, a noninterference property, and the termination of the analysis.