pith. sign in

arxiv: 1906.11507 · v1 · pith:DQDHNS3Inew · submitted 2019-06-27 · 💻 cs.CR

An Empirical Study of Information Flows in Real-World JavaScript

Cristian-Alexandru Staicu , Daniel Schoepe , Musard Balliu , Michael Pradel , Andrei Sabelfeld This is my paper

Pith reviewed 2026-05-25 14:53 UTC · model grok-4.3

classification 💻 cs.CR
keywords information flow analysisJavaScripttaint analysisimplicit flowsdynamic analysissecurity vulnerabilitiesprivacy leaks
0
0 comments X

The pith

Lightweight taint analysis catches most security problems in real-world JavaScript programs while tracking hidden implicit flows adds cost without benefit.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

This paper examines how different kinds of information flows appear in 56 real-world JavaScript programs that have security issues. It compares lightweight taint analysis, which tracks only explicit flows, to heavier approaches that also consider implicit flows from control flow, including hidden ones from unexecuted branches. The study finds that implicit flows are costly to track due to reduced permissiveness, label creep, and runtime overhead. A lightweight approach proves sufficient for most problems like code injection and denial of service, with observable implicit flows helping in some privacy cases. No evidence emerges that hidden implicit flows catch security problems missed by lighter methods. These results matter for deciding how much tracking to implement in practical security tools for JavaScript.

Core claim

In an empirical study of 56 JavaScript programs with security problems, dynamic information flow analysis shows that implicit flows are expensive to track fully, a lightweight taint analysis suffices for most issues, observable tracking is needed for some privacy code, and hidden implicit flows do not reveal otherwise missed security problems.

What carries the argument

Dynamic information flow analysis with varying granularity levels applied to real-world programs

If this is right

  • Most security problems in the studied programs can be addressed without tracking implicit flows.
  • Observable implicit flows are sometimes necessary for privacy-related code.
  • Tracking hidden implicit flows increases overhead in permissiveness, label creep, and runtime without catching additional issues.
  • The cost-benefit tradeoffs favor lighter analyses for the examined security problems.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • Analysis designers may prioritize developing cost-effective methods for handling implicit flows rather than full tracking.
  • Security tools for JavaScript could default to taint analysis unless privacy concerns require more.
  • Future empirical studies might test these findings on larger or different sets of programs.

Load-bearing premise

The selection of 56 real-world JavaScript programs with security problems is representative for general conclusions on information flow tracking tradeoffs.

What would settle it

A single documented case of a real-world JavaScript program where a security vulnerability is only detected by tracking hidden implicit flows would falsify the main finding.

Figures

Figures reproduced from arXiv: 1906.11507 by Andrei Sabelfeld, Cristian-Alexandru Staicu, Daniel Schoepe, Michael Pradel, Musard Balliu.

Figure 1
Figure 1. Figure 1: Program leaking the password to the network. [PITH_FULL_IMAGE:figures/full_fig_p001_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Rules for NanoJS with flow counting. insensitive sinks, any write of an expression with non-zero flow counts will result in incrementing the global counters. Security conditions: We also adapt existing security condi￾tions for tracking only explicit or observable flows to NanoJS [7]. To capture only explicit flows, we use the notion of explicit secrecy; intu￾itively, a run of a program satisfies explicit s… view at source ↗
Figure 3
Figure 3. Figure 3: Prevalence of micro flows. 0 1 2 3 4 5 6 7 1 2 3 4 5 6 7 8 9 10111213141516171819202122 232425 2627 28 29 3031 32 333435 363738 3940 4142 4344 45 46 4748 495051 5253 545556 Injections ReDoS Buffer Fingerprinting Number of source-to-sink flows Benchmark Taint Tracking Observable Tracking Permissive Upgrade [PITH_FULL_IMAGE:figures/full_fig_p009_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: Number of source-to-sink flows detected at different security modes. [PITH_FULL_IMAGE:figures/full_fig_p009_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: Number of violations, summarized by code loca [PITH_FULL_IMAGE:figures/full_fig_p009_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: LCR over execution time 1 // query marked 'sensitive ': 2 function parseQuery ( query ) { 3 // query pushed on the stack : 4 if( query instanceof Function ) { 5 var nF = eval ( query ) ; // sink call 6 return [new Part (null , '$', nF) ]; 7 } 8 } 9 function Part (f, operator , operand , p) { 10 if(p === undefined ) 11 p = []; // implicit 12 this . field = f; // implicit 13 this . operator = operator ; // i… view at source ↗
Figure 7
Figure 7. Figure 7: Implicit flows snippet from benchmark 11. [PITH_FULL_IMAGE:figures/full_fig_p010_7.png] view at source ↗
read the original abstract

Information flow analysis prevents secret or untrusted data from flowing into public or trusted sinks. Existing mechanisms cover a wide array of options, ranging from lightweight taint analysis to heavyweight information flow control that also considers implicit flows. Dynamic analysis, which is particularly popular for languages such as JavaScript, faces the question whether to invest in analyzing flows caused by not executing a particular branch, so-called hidden implicit flows. This paper addresses the questions how common different kinds of flows are in real-world programs, how important these flows are to enforce security policies, and how costly it is to consider these flows. We address these questions in an empirical study that analyzes 56 real-world JavaScript programs that suffer from various security problems, such as code injection vulnerabilities, denial of service vulnerabilities, memory leaks, and privacy leaks. The study is based on a state-of-the-art dynamic information flow analysis and a formalization of its core. We find that implicit flows are expensive to track in terms of permissiveness, label creep, and runtime overhead. We find a lightweight taint analysis to be sufficient for most of the studied security problems, while for some privacy-related code, observable tracking is sometimes required. In contrast, we do not find any evidence that tracking hidden implicit flows reveals otherwise missed security problems. Our results help security analysts and analysis designers to understand the cost-benefit tradeoffs of information flow analysis and provide empirical evidence that analyzing implicit flows in a cost-effective way is a relevant problem.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 1 minor

Summary. The paper presents an empirical study of information flow tracking options (taint analysis, observable implicit flows, and hidden implicit flows) in 56 real-world JavaScript programs that exhibit security problems such as code injection, DoS, memory leaks, and privacy leaks. It uses a state-of-the-art dynamic analysis together with a formalization of its core to measure prevalence, security relevance, and costs (permissiveness, label creep, runtime overhead). The central claims are that implicit flows are expensive to track, lightweight taint analysis suffices for most studied problems, observable tracking is sometimes required for privacy-related code, and hidden implicit flows provide no evidence of revealing otherwise missed security problems.

Significance. If the results hold, the work supplies concrete empirical data on the cost-benefit tradeoffs of information-flow granularities in JavaScript, which can guide designers of practical security tools. The combination of dynamic analysis with a formalization of its core is a methodological strength that increases confidence in the measurements.

major comments (2)
  1. [Abstract and §3 (study design)] Abstract and program-selection description: the central negative claim ('we do not find any evidence that tracking hidden implicit flows reveals otherwise missed security problems') rests on a corpus of 56 programs that were chosen precisely because they already suffer from identifiable security problems. By construction, those problems were detectable without hidden-implicit tracking; the study therefore provides no separate search over a broader or unbiased corpus for vulnerabilities whose only information-flow path is hidden implicit. This selection weakens support for the general cost-benefit conclusion.
  2. [§3 and §4] §3 and §4 (measurement methodology): the high-level summary leaves the exact program-selection criteria, the precise definition and counting of each flow type, and the statistical handling of results unstated. These details are load-bearing for the quantitative claims about prevalence, label creep, and overhead.
minor comments (1)
  1. [Abstract] Abstract: the sentence on 'various security problems' would be clearer if it listed the four categories (injection, DoS, memory leaks, privacy leaks) explicitly.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the detailed and constructive comments. We address each major point below and indicate where revisions will be made to the manuscript.

read point-by-point responses

  1. Referee: [Abstract and §3 (study design)] Abstract and program-selection description: the central negative claim ('we do not find any evidence that tracking hidden implicit flows reveals otherwise missed security problems') rests on a corpus of 56 programs that were chosen precisely because they already suffer from identifiable security problems. By construction, those problems were detectable without hidden-implicit tracking; the study therefore provides no separate search over a broader or unbiased corpus for vulnerabilities whose only information-flow path is hidden implicit. This selection weakens support for the general cost-benefit conclusion.

    Authors: We agree that selecting programs already known to have security problems detectable without hidden implicit flows limits the strength of the negative claim. The study shows no additional problems were revealed by hidden flows in this corpus, but cannot address whether such flows would be the sole path in an unbiased search over all programs. We will revise the abstract and the discussion of limitations in §5 to state the scope more precisely and explicitly note this corpus limitation. This change will be incorporated. revision: yes

  2. Referee: [§3 and §4] §3 and §4 (measurement methodology): the high-level summary leaves the exact program-selection criteria, the precise definition and counting of each flow type, and the statistical handling of results unstated. These details are load-bearing for the quantitative claims about prevalence, label creep, and overhead.

    Authors: Section 3.1 details the selection criteria (programs drawn from CVE entries, security benchmarks, and vulnerability reports exhibiting the listed issue types). Flow definitions and counting are given by the formalization in §2 together with the instrumentation rules in §4.1–4.3; results report per-program values plus aggregate statistics (means and distributions) in the tables and figures of §4. We will add cross-references from the abstract and introduction to these subsections and include a short methodology summary paragraph to make the details more immediately visible. This revision will be made. revision: yes

Circularity Check

0 steps flagged

No circularity: purely empirical study with no derivations or self-referential predictions

full rationale

The paper performs an empirical analysis of information flows in 56 pre-selected real-world JavaScript programs using a state-of-the-art dynamic analysis. Its central claims (implicit flows are expensive; taint analysis suffices for most studied problems; no evidence for hidden implicit flows revealing missed issues) are direct observations from running the analysis on the chosen corpus. No equations, fitted parameters, predictions derived from inputs, or load-bearing self-citations appear in the provided text. The selection of programs with known security problems is an explicit methodological choice whose limitations are acknowledged in the reader's take, but this does not constitute circularity in any derivation chain because there is no derivation chain to reduce. The study is self-contained against external benchmarks via its direct measurements.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The central claims rest on the assumption that the chosen dynamic analysis correctly implements the formalized information flow semantics and that the 56 programs form a suitable sample for drawing conclusions about real-world JavaScript security analysis tradeoffs.

axioms (2)
  • domain assumption The state-of-the-art dynamic information flow analysis used in the study accurately tracks the defined categories of flows.
    Invoked when the study bases its measurements on this tool.
  • domain assumption The 56 programs suffering from security problems are representative of real-world JavaScript applications.
    Required to generalize the cost-benefit findings beyond the specific corpus.

pith-pipeline@v0.9.0 · 5807 in / 1301 out tokens · 23311 ms · 2026-05-25T14:53:15.692219+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

70 extracted references · 70 canonical work pages

  1. [1]

    Babel JavaScript compiler

    Accessed: 2018-02-08. Babel JavaScript compiler. https://babeljs.io

    work page 2018

  2. [2]

    Gunes Acar, Christian Eubank, Steven Englehardt, Marc Juárez, Arvind Narayanan, and Claudia Díaz. 2014. The Web Never Forgets: Persistent Tracking Mechanisms in the Wild. In Proceedings of the 2014 ACM SIGSAC Conference on Computer and Communications Security, Scottsdale, AZ, USA, November 3-7, 2014 . 674–689

    work page 2014

  3. [3]

    Gunes Acar, Marc Juarez, Nick Nikiforakis, Claudia Diaz, Seda Gürses, Frank Piessens, and Bart Preneel. 2013. FPDetective: dusting the web for fingerprinters. In Proceedings of the 2013 ACM SIGSAC conference on Computer & communications security. ACM, 1129–1140

    work page 2013

  4. [4]

    Austin and Cormac Flanagan

    Thomas H. Austin and Cormac Flanagan. 2009. Efficient purely-dynamic infor- mation flow analysis. In Workshop on Programming Languages and Analysis for Security (PLAS 2009). ACM, 113–124

    work page 2009

  5. [5]

    Austin and Cormac Flanagan

    Thomas H. Austin and Cormac Flanagan. 2010. Permissive dynamic information flow analysis. In Workshop on Programming Languages and Analysis for Security (PLAS 2010). ACM, 3

    work page 2010

  6. [6]

    Austin and Cormac Flanagan

    Thomas H. Austin and Cormac Flanagan. 2012. Multiple Facets for Dynamic Information Flow. In Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’12) . 165–178

    work page 2012

  7. [7]

    Musard Balliu, Daniel Schoepe, and Andrei Sabelfeld. 2017. We Are Family: Relating Information-Flow Trackers. In Computer Security - ESORICS 2017 - 22nd European Symposium on Research in Computer Security, Oslo, Norway, September 11-15, 2017, Proceedings, Part I . 124–145

    work page 2017

  8. [8]

    Tao Bao, Yunhui Zheng, Zhiqiang Lin, Xiangyu Zhang, and Dongyan Xu. 2010. Strict control dependence and its effect on dynamic information flow analyses. In International Symposium on Software Testing and Analysis (ISSTA 2010) . ACM, 13–24

    work page 2010

  9. [9]

    Lujo Bauer, Shaoying Cai, Limin Jia, Timothy Passaro, Michael Stroucken, and Yuan Tian. 2015. Run-time Monitoring and Formal Analysis of Information Flows in Chromium. InNetwork and Distributed System Security Symposium (NDSS 2015). The Internet Society

    work page 2015

  10. [10]

    Abhishek Bichhawat, Vineet Rajani, Deepak Garg, and Christian Hammer. 2014. Information Flow Control in WebKit’s JavaScript Bytecode. InPrinciples of Secu- rity and Trust (POST 2014) (LNCS) , Vol. 8414. Springer, 159–178

    work page 2014

  11. [11]

    Abhishek Bichhawat, Vineet Rajani, Jinank Jain, Deepak Garg, and Christian Ham- mer. 2017. WebPol: Fine-Grained Information Flow Policies for Web Browsers. In Computer Security - ESORICS 2017 - 22nd European Symposium on Research in Computer Security, Oslo, Norway, September 11-15, 2017, Proceedings, Part I . 242–259

    work page 2017

  12. [12]

    Arnar Birgisson, Daniel Hedin, and Andrei Sabelfeld. 2012. Boosting the permis- siveness of dynamic information-flow tracking by testing. In European Sympo- sium on Research in Computer Security (ESORICS 2012) . LNCS, Vol. 7459. Springer, 55–72

    work page 2012

  13. [13]

    Deepak Chandra and Michael Franz. 2007. Fine-Grained Information Flow Anal- ysis and Enforcement in a Java Virtual Machine. In Annual Computer Security Applications Conference (ACSAC 2007). IEEE, 463–475

    work page 2007

  14. [14]

    Andrey Chudnov and David A. Naumann. 2015. Inlined Information Flow Mon- itoring for JavaScript. In ACM Conference on Computer and Communications Security (CCS 2015). ACM, 629–643

    work page 2015

  15. [15]

    Meister, Ranjit Jhala, and Sorin Lerner

    Ravi Chugh, Jeffrey A. Meister, Ranjit Jhala, and Sorin Lerner. 2009. Staged infor- mation flow for JavaScript. In Programming Language Design and Implementation (PLDI 2009). ACM, 50–62

    work page 2009

  16. [16]

    Clause, Wanchun Li, and Alessandro Orso

    James A. Clause, Wanchun Li, and Alessandro Orso. 2007. Dytan: a generic dynamic taint analysis framework. InInternational Symposium on Software Testing and Analysis (ISSTA 2007). ACM, 196–206

    work page 2007

  17. [17]

    Willem De Groef, Dominique Devriese, Nick Nikiforakis, and Frank Piessens. 2012. FlowFox: A Web Browser with Flexible and Precise Information Flow Control. In Proceedings of the 2012 ACM Conference on Computer and Communications Security (CCS ’12). 748–759

    work page 2012

  18. [18]

    Dorothy Denning. 1982. Cryptography and Data Security . Addison-Wesley Longman Publishing Co., Inc., Boston, MA, USA

    work page 1982

  19. [19]

    Dorothy E. Denning. 1976. A Lattice Model of Secure Information Flow.Commun. ACM 19, 5 (1976), 236–243

    work page 1976

  20. [20]

    Denning and Peter J

    Dorothy E. Denning and Peter J. Denning. 1977. Certification of programs for secure information flow. Commun. ACM 20, 7 (1977), 504–513

    work page 1977

  21. [21]

    Mohan Dhawan and Vinod Ganapathy. 2009. Analyzing information flow in JavaScript-based browser extensions. In Annual Computer Security Applications Conference (ACSAC 2009). IEEE, 382–391

    work page 2009

  22. [22]

    Alex Halderman, Michael Bailey, Frank Li, Nicholas Weaver, Johanna Amann, Jethro Beekman, Mathias Payer, and Vern Paxson

    Zakir Durumeric, James Kasten, David Adrian, J. Alex Halderman, Michael Bailey, Frank Li, Nicholas Weaver, Johanna Amann, Jethro Beekman, Mathias Payer, and Vern Paxson. 2014. The Matter of Heartbleed. InInternet Measurement Conference (IMC). 475–488

    work page 2014

  23. [23]

    J. S. Fenton. 1974. Memoryless Subsystems. Comput. J. 17, 2 (1974), 143–147

    work page 1974

  24. [24]

    J. A. Goguen and J. Meseguer. 1982. Security Policies and Security Models.. In S&P

    work page 1982

  25. [25]

    Daniel Hedin, Arnar Birgisson, Luciano Bello, and Andrei Sabelfeld. 2014. JSFlow: Tracking information flow in JavaScript and its APIs. In Symposium on Applied Computing (SAC 2014). ACM, 1663–1671

    work page 2014

  26. [26]

    Daniel Hedin and Andrei Sabelfeld. 2012. Information-Flow Security for a Core of JavaScript. In Computer Security Foundations Symposium (CSF 2012) . IEEE, 3–18

    work page 2012

  27. [27]

    Dongseok Jang, Ranjit Jhala, Sorin Lerner, and Hovav Shacham. 2010. An empiri- cal study of privacy-violating information flows in JavaScript web applications. In ACM Conference on Computer and Communications Security (CCS 2010) . ACM, 270–283

    work page 2010

  28. [28]

    D. Jang, R. Jhala, S. Lerner, and H. Shacham. 2010. An empirical study of privacy- violating information flows in JavaScript web applications. In CCS

    work page 2010

  29. [29]

    Martin Johns. 2008. On JavaScript Malware and related threats. Journal in Computer Virology 4, 3 (2008), 161–178

    work page 2008

  30. [30]

    Min Gyung Kang, Stephen McCamant, Pongsin Poosankam, and Dawn Song

    work page

  31. [31]

    DTA++: Dynamic Taint Analysis with Targeted Control-Flow Propagation. In NDSS

    work page

  32. [32]

    Christoph Kerschbaumer, Eric Hennigan, Per Larsen, Stefan Brunthaler, and Michael Franz. 2013. CrowdFlow: Efficient Information Flow Security. In ISC (Lecture Notes in Computer Science) , Vol. 7807. Springer, 321–337

    work page 2013

  33. [33]

    Dave King, Boniface Hicks, Michael Hicks, and Trent Jaeger. 2008. Implicit Flows: Can’t Live with ’Em, Can’t Live without ’Em. InInternational Conference on Information Systems Security (ICISS 2008) (LNCS) , Vol. 5352. Springer, 56–70

    work page 2008

  34. [34]

    Sebastian Lekies, Ben Stock, and Martin Johns. 2013. 25 million flows later: large-scale detection of DOM-based XSS. In ACM Conference on Computer and Communications Security (CCS 2013) . ACM, 1193–1204

    work page 2013

  35. [35]

    Wes Masri and Andy Podgurski. 2009. Measuring the strength of information flows in programs. ACM Transactions on Software Engineering and Methodology (TOSEM) 19, 2 (2009)

    work page 2009

  36. [36]

    William Melicher, Anupam Das, Mahmood Sharif, Lujo Bauer, and Limin Jia. 2018. Riding out DOMsday: Toward detecting and preventing DOM cross-site scripting. In Proceedings of the 25th Network and Distributed System Security Symposium . https://doi.org/10.14722/ndss.2018.23309 To appear

    work page doi:10.14722/ndss.2018.23309 2018

  37. [37]

    Myers and Barbara Liskov

    Andrew C. Myers and Barbara Liskov. 2000. Protecting privacy using the decen- tralized label model. ACM Transactions on Software Engineering and Methodology (TOSEM) 9, 4 (2000), 410–442

    work page 2000

  38. [38]

    Nick Nikiforakis, Alexandros Kapravelos, Wouter Joosen, Christopher Kruegel, Frank Piessens, and Giovanni Vigna. 2013. Cookieless Monster: Exploring the Ecosystem of Web-Based Device Fingerprinting. In 2013 IEEE Symposium on Security and Privacy, SP 2013, Berkeley, CA, USA, May 19-22, 2013 . 541–555

    work page 2013

  39. [39]

    Russo, A

    A. Russo, A. Sabelfeld, and K. Li. 2009. Implicit flows in malicious and nonmali- cious code. Marktoberdorf Summer School (IOS Press) (2009)

    work page 2009

  40. [40]

    Andrei Sabelfeld and Andrew C. Myers. 2003. Language-Based Information-Flow Security. IEEE Journal on Selected Areas in Communications 21, 1 (2003), 5–19

    work page 2003

  41. [41]

    Prateek Saxena, Steve Hanna, Pongsin Poosankam, and Dawn Song. 2010. FLAX: Systematic Discovery of Client-side Validation Vulnerabilities in Rich Web Ap- plications. In Network and Distributed System Security Symposium (NDSS 2010) . The Internet Society

    work page 2010

  42. [42]

    Schoepe, M

    D. Schoepe, M. Balliu, B. C. Pierce, and A. Sabelfeld. 2016. Explicit Secrecy: A Policy for Taint Tracking. In EuroS&P

    work page 2016

  43. [43]

    Schwartz, Thanassis Avgerinos, and David Brumley

    Edward J. Schwartz, Thanassis Avgerinos, and David Brumley. 2010. All You Ever Wanted to Know about Dynamic Taint Analysis and Forward Symbolic Execution (but Might Have Been Afraid to Ask). In IEEE S&P

    work page 2010

  44. [44]

    Koushik Sen, Swaroop Kalasapur, Tasneem Brutch, and Simon Gibbs. 2013. Jalangi: A Selective Record-Replay and Dynamic Analysis Framework for JavaScript. In European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE 2013) . ACM, 488–498

    work page 2013

  45. [45]

    Alexander Sjösten, Steven Van Acker, and Andrei Sabelfeld. 2017. Discovering Browser Extensions via Web Accessible Resources. In Proceedings of the Seventh ACM on Conference on Data and Application Security and Privacy, CODASPY 2017, Scottsdale, AZ, USA, March 22-24, 2017 . 329–336

    work page 2017

  46. [46]

    Cristian-Alexandru Staicu and Michael Pradel. 2018. Freezing the Web: A Study of ReDoS Vulnerabilities in JavaScript-based Web Servers. In USENIX Security Symposium. 361–376. 12

    work page 2018

  47. [47]

    Cristian-Alexandru Staicu, Michael Pradel, and Ben Livshits. 2018. Understanding and Automatically Preventing Injection Attacks on Node.js. In NDSS

    work page 2018

  48. [48]

    Omer Tripp, Pietro Ferrara, and Marco Pistoia. 2014. Hybrid Security Analysis of Web JavaScript Code via Dynamic Partial Evaluation. In ISSTA

    work page 2014

  49. [49]

    Philipp Vogt, Florian Nentwich, Nenad Jovanovic, Engin Kirda, Christopher Krügel, and Giovanni Vigna. 2007. Cross Site Scripting Prevention with Dynamic Data Tainting and Static Analysis. In Proceedings of the Network and Distributed System Security Symposium, NDSS 2007, San Diego, California, USA, 28th February - 2nd March 2007

    work page 2007

  50. [50]

    Zachary Weinberg, Eric Y Chen, Pavithra Ramesh Jayaraman, and Collin Jackson

    work page

  51. [51]

    In Security and Privacy (SP), 2011 IEEE Symposium on

    I still know what you visited last summer: Leaking browsing history via user interaction and side channel attacks. In Security and Privacy (SP), 2011 IEEE Symposium on. IEEE, 147–161

    work page 2011

  52. [52]

    Stephan Zdancewic. 2002. Programming Languages for Information Security. Ph.D. Dissertation. Cornell University, Ithaca, NY, USA. A SECURITY DEFINITIONS The previous section has formally defined the flow counting that is at the heart of our empirical study. We now related the flow count- ing to three previously described [7] security conditions: Explicit ...

    work page 2002

  53. [53]

    Formally, (ρ1, h1) ≤ (ρ2, h2) iff ∀xv1κ1v2κ2

    ⊆ Stmt where ce ∈ B iff whenever (ρ0, h0) ≤ ( ρ, h), (ρ0, h0) =L (ρ, h), and ⟨ce ,ρ, h, [],κ0⟩ τ − → ⋆ ⟨ε,ρ′, h′, t ′,κ′⟩, then (ρ′, h′) ≤ ( env ′ 0, h′ 0), where (ρ, h) ≤ ( ρ0, h0) iff the counter of each value in ρand h is related by ⊑ to the corresponding counter inρ0 and h0. Formally, (ρ1, h1) ≤ (ρ2, h2) iff ∀xv1κ1v2κ2. ρ1(x) =vκ1 1 ∧ρ2(x) =vκ2 2 ⇒ κ1...

    work page

  54. [54]

    If it is low, it follows from the previous fact that x also receives 0 inρ′′, h′′

    is not 0, then the claim follows trivially. If it is low, it follows from the previous fact that x also receives 0 inρ′′, h′′. Case E-AssignField is analogous. Case E-Sink: In this case c ′e ∈ B(ρ0, h0,ρ′′ 0 , h′′ 0 ) follows easily from the induction hypothesis as the sink statement does not change the environment and heap. c ′e ∈ IE (ρ0, h0) follows tri...

    work page

  55. [55]

    • Moreover, (ρ′, h′) =W (ρ′ 2, h′

    = π1,2(κ′) (1) and • There existρ′ 2, h′ 2, t ′ 2,κ′ 2 and S ′ 2 such that (⟨ce ,ρ2, h2, [],κ0 τ − → ⋆ ⟨• ; poplength(t ′),ρ′ 2, h′ 2, t ′ 2,κ′ 2⟩⟩ ∧ length(t ′) = length(t ′ 2)) ∨ (⟨ce , ρ2, h2, [],κ0⟩ τ − → ⋆ ⟨ε, h′ 2, t ′ 2,κ′ 2⟩ ∧ Ã t ′ = H) (2). • Moreover, (ρ′, h′) =W (ρ′ 2, h′

    work page

  56. [56]

    ≤ (ρ′, h′), and t ′ 2 ⪯ t ′. (3) whereρ1 =W ρ2 holds iff all values labeled low in both environ- ments are equal in value and lists of levelsxs andys satisfy xs ⪯ys if there exists a suffix of length length(xs ) ofys such that all levels are pairwise related by ⊑. We write cn for n copies of c composed with sequential composition. We show this by inductio...

    work page

  57. [57]

    ≤ ( ρ′, h′), and t ′ 2 ⪯ t ′. We show (1 − 3) by induction on (⟨c ′,ρ′, h′, t ′,κ′⟩, ce ) τ′ − − → (⟨c ′′,ρ′′, h′′, t ′′,κ′′⟩, c ′e ); the interesting cases are E-Assign, E-AssignField, E-IfTrue/False, E-Sink, and E-Pop. We refer to the proof obligations as (1′′′), (2′′′), and (3′′′). Case E-Assign: (1′′) follows trivially from the semantics. We have c ′e...

    work page

  58. [58]

    In the case where ⟨c ′e ,ρ2, h2, [],κ0⟩ τ − → ⋆ ⟨ε,ρ′ 2, h′ 2, t ′ 2,κ′ 2⟩, then we have that Ã(t ′) , 0

    = length(t ′) follows from this case in (2′) and the fact that assignments do not modify the label stack. In the case where ⟨c ′e ,ρ2, h2, [],κ0⟩ τ − → ⋆ ⟨ε,ρ′ 2, h′ 2, t ′ 2,κ′ 2⟩, then we have that Ã(t ′) , 0. Therefore, we have that the counter of ρ′′(x) is not 0, therefore (ρ′′ 2 , h′

    work page

  59. [59]

    =W (ρ′′, h′′) and (ρ′′ 2 , h′

    work page

  60. [60]

    The other statements follow from the induction hypothesis: If • is not reached, then ce [c2] matches the evaluation of ce for any c2

    ≤ (ρ′′, h′′) follows trivially. The other statements follow from the induction hypothesis: If • is not reached, then ce [c2] matches the evaluation of ce for any c2. Case E-AssignField: Analogous to E-Assign. Case E-If: Without loss of generality, we only discuss the case where the then branch is taken. In this case, we first note thatρ′′ = ρ′, h′′ = h′ a...

    work page

  61. [61]

    Note that for JeK(ρ′ 2, h′

    = length(t ′), then we have that ⟨c ′e ,ρ2, h2, [],κ0⟩ τ − → ⋆ ⟨if (e) { • } else { skip } ; poplength(t ′),ρ′ 2, h′ 2, t ′ 2,κ′ 2⟩. Note that for JeK(ρ′ 2, h′

    work page

  62. [62]

    = vκ2 e 2 and (ρ′ 2, h′

    work page

  63. [63]

    To show(2′′) we proceed by case distinction onv2 = tt

    ≤ (ρ′, h′) we have thatκ2e ⊑κe . To show(2′′) we proceed by case distinction onv2 = tt. Ifv2 = tt, we have that⟨if (e) { • } else { skip } ; poplength(t ′),ρ′ 2, h′ 2, t ′′ 2 ,κ′ 2⟩ [] − → ⟨• ; poplength(t ′)+1,ρ′ 2, h′ 2, t ′′ 2 ,κ′ 2⟩ where t ′′ 2 =κ2e .t ′

    work page

  64. [64]

    Sinceκ2e ⊑κe , we have that t ′′ 2 ⪯ t ′′; we also have that length(t ′′ 2 ) = length(t ′′) trivially. In the case wherev2 , tt, we have that⟨if (e) { • } else { skip } ; poplength(t ′),ρ′ 2, h′ 2, t ′′ 2 ,κ′ 2⟩ [] − → ⟨skip ; poplength(t ′)+1,ρ′ 2, h′ 2, t ′′ 2 , κ′ 2⟩ [] − → ⋆ ⟨ε,ρ′ 2, h′ 2, t ′′′ 2 ,κ′ 2⟩ where t ′′′ 2 is a prefix of t ′′ 2 and hence, ...

    work page

  65. [65]

    wherev2e is the result of evaluating e in ρ′ 2, h′

    =W (ρ′, h′), we have that κ′′ , 0 as required for this case. wherev2e is the result of evaluating e in ρ′ 2, h′

    work page

  66. [66]

    = length(t ′) follows from this case in(2′) and the fact that assignments do not modify the label stack. In the case where ⟨ce ,ρ2, h2, [],κ0⟩ τ − → ⋆ ⟨ε,ρ′ 2, h′ 2, t ′ 2,κ′ 2⟩ and Ã(t ′) , 0, we have that then⟨c ′e ,ρ2, h2, [],κ0⟩ τ − → ⋆ ⟨ε,ρ′ 2, h′ 2, t ′ 2,κ′ 2⟩ since • is not reached and hence replacing it withif (e) { • } else { skip } does not aff...

    work page

  67. [67]

    Hence we also have that ⟨c ′e ,ρ2, h2, [],κ0⟩ τ − → ⋆ ⟨sink(e) ; • ; poplength(t ′ 2),ρ′ 2, h′ 2, t ′ 2,κ′ 2⟩ v2 − − → ⟨• ; poplength(t ′ 2),ρ2, h2, t2,κ′ 2⟩

    = length(t ′). Hence we also have that ⟨c ′e ,ρ2, h2, [],κ0⟩ τ − → ⋆ ⟨sink(e) ; • ; poplength(t ′ 2),ρ′ 2, h′ 2, t ′ 2,κ′ 2⟩ v2 − − → ⟨• ; poplength(t ′ 2),ρ2, h2, t2,κ′ 2⟩. Since π1,2(κ′′) = 0, we also have that the label ofv is 0; from (ρ′ 2, h′

    work page

  68. [68]

    With (ρ′, h′) =W (ρ′ 2, h′

    ≤ ( ρ′, h′) we have thatv2 is also labeled 0. With (ρ′, h′) =W (ρ′ 2, h′

    work page

  69. [69]

    (3′′) follows easily since heaps, environments, and the label stack are not modified by executing a sink statement

    this yields that v = v2, concluding (2′′). (3′′) follows easily since heaps, environments, and the label stack are not modified by executing a sink statement. Case E-Pop: By this case we have c ′e = leaveBranch(ce ). (1′′) follows easily. For (2′′) we again proceed by case distinction on the disjunction in (2′). In the first case, the conclusion follows e...

    work page

  70. [70]

    This stronger property then trivially implies non-interference of ce [skip]

    , ttκ2 for anyκ2, and, since c2 = skip, we reach • ; poplength(t ′′) trivially, concluding the induction. This stronger property then trivially implies non-interference of ce [skip]. □ 15

    work page