Type-based Dependency Analysis

by Matthias Keil and Peter Thiemann

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.

Software Download

• git clone https://github.com/keil/TbDA.git

Publications

Research Paper

• Matthias Keil and Peter Thiemann
  
  Type-based Dependency Analysis for JavaScript
  
  ACM SIGPLAN Eighth Workshop on Programming Languages and Analysis for Security
  
  PLAS'13, Seattle, WA, USA
  
  
  
   
• Matthias Keil and Peter Thiemann
  
  Type-based Dependency Analysis for JavaScript (Technical Report)
  
  Institute for Computer Science, University of Freiburg, 2013
  
  
  
   

Talks

• Matthias Keil
  
  Type-based Dependency Analysis for JavaScript
  
  ACM SIGPLAN Eighth Workshop on Programming Languages and Analysis for Security, PLAS'13
  
  Seattle, WA, USA, June 20, 2013
  
  
  
   
• Matthias Keil
  
  Type-Based Dependency Analysis
  
  RS³ Topic Workshop on Concurrent Noninterference
  
  Darmstadt, Germany, June 2012