iflowTYPES.js Typing Secure Information Flow in JavaScript

Introduction Type Checker Case Study

Introduction

iflowtypes.js is a JavaScript library designed to type secure information flow in JavaScript. iflowtypes.js has two main modes of operation: fully static and hybrid. In the hybrid mode, the program to be typed is instrumented with runtime assertions that are verified at runtime. By deferring rejection to runtime, the hybrid type system is able to type more programs than fully static mechanisms.

iflowtypes.js was designed as a didactical tool to support the paper...

Techical details can be found in the paper From Static to Hybrid Information Flow Control in Core of JavaScript.

Type-Checker

Load example:   Category:   File:  
Processing options

Action type:  

Input script:
Output:

See:

Type of the Output:
Instrumented Script:
Typing Environment



My Types

Source code available here.

Notes:

Contact Manager

Here we present the code for a simple Contact Manager application as well as the security types required for typing it. You can change both the security types and the code and retype it. You can also run it.

Security Types:


Contact Manager Code:

Processing Options

Action:  

Value 3
Variable - 1 h l: PRIM^{0} h: PRIM^{5}
Variable - 2 l l: PRIM^{0} h: PRIM^{5}
Binary Operatorion - 1 l0 + h; l0: PRIM^{0} l1: PRIM^{0} h: PRIM^{1}
Binary Operatorion - 2 l0 + l1; l0: PRIM^{0} l1: PRIM^{0} l2: PRIM^{0}
Unary Operatorion - 1 !l l: PRIM^{0}
Unary Operatorion - 2 !h h: PRIM^{5}
Variable Assign - 1 h = l l: PRIM^{0} h: PRIM^{5}
Variable Assign - 2 l = h l: PRIM^{0} h: PRIM^{5}
Variable Assign - 3 l1 = l1 + l2 l1: PRIM^{0} l2: PRIM^{0} h: PRIM^{5}
Variable Assign - 4 l1 = l1 + h l1: PRIM^{0} l2: PRIM^{0} h: PRIM^{5}
Variable Assign - 5 h = l1 + l2 + h l1: PRIM^{0} l2: PRIM^{0} h: PRIM^{5}
Sequence - 1 l1 = l1 + l2, h = l1 l1: PRIM^{0} l2: PRIM^{0} h: PRIM^{5}
Sequence - 2 l1 = l1 + l2, l2 = h l1: PRIM^{0} l2: PRIM^{0} h: PRIM^{5}
Conditional - 1 l1 ? h = l1 - l2 : h = l2 - l1; l1: PRIM^{0} l2: PRIM^{0} h: PRIM^{5}
Conditional - 2 h ? l1 = 9 : h = l2 - l1; l1: PRIM^{0} l2: PRIM^{0} h: PRIM^{5}
Object Literal o = {}; l: PRIM^{0} y: PRIM^{0} o: OBJ<__k>< p1^{0}: PRIM^{3}, p2^{0}: PRIM^{2}, *^{0}: PRIM^{0}>^{0}
Property Look-up - 1 l = o[y]; l: PRIM^{0} y: PRIM^{0} o: OBJ<__k>< p1^{0}: PRIM^{3}, p2^{0}: PRIM^{2}, *^{0}: PRIM^{0}>^{0}
Property Look-up - 2 l = o[y @ <STR>]; l: PRIM^{0} y: PRIM^{0} o: OBJ<__k>< p1^{0}: PRIM^{3}, p2^{0}: PRIM^{2}, *^{0}: PRIM^{0}>^{0}
Property Look-up - 3 l = o[y @ {p3, p4}]; l: PRIM^{0} y: PRIM^{0} o: OBJ<__k>< p1^{0}: PRIM^{3}, p2^{0}: PRIM^{2}, *^{0}: PRIM^{0}>^{0}
Property Look-up - 4 l = o[y @ {p1, p5}]; l: PRIM^{0} y: PRIM^{0} o: OBJ<__k>< p1^{0}: PRIM^{3}, p2^{0}: PRIM^{2}, *^{0}: PRIM^{0}>^{0}
Property Look-up - 5 h = o[y]; h: PRIM^{5} y: PRIM^{0} o: OBJ<__k>< p1^{0}: PRIM^{3}, p2^{0}: PRIM^{0}, *^{0}: PRIM^{1}>^{0}
In Expression - 1 l = y in o; l: PRIM^{0} y: PRIM^{0} o: OBJ<__k>< p1^{0}: PRIM^{3}, p2^{0}: PRIM^{0}, *^{0}: PRIM^{1}>^{0}
In Expression - 2 l = y in o; l: PRIM^{0} y: PRIM^{0} o: OBJ<__k>< p1^{2}: PRIM^{3}, p2^{0}: PRIM^{0}, *^{0}: PRIM^{1}>^{0}
In Expression - 3 l = y in o; l: PRIM^{0} y: PRIM^{1} o: OBJ<__k>< p1^{2}: PRIM^{3}, p2^{0}: PRIM^{0}, *^{0}: PRIM^{1}>^{0}
In Expression - 4 l = y in^@{p1, p4} o; l: PRIM^{0} y: PRIM^{0} o: OBJ<__k>< p1^{2}: PRIM^{3}, p2^{0}: PRIM^{0}, *^{0}: PRIM^{1}>^{0}
Property Assign - 1 o1[y] = o2[x]; x: PRIM^{0} y: PRIM^{0} o1: OBJ<__k>< p1^{2}: PRIM^{3}, p2^{0}: PRIM^{0}, *^{0}: PRIM^{1}>^{0} o2: OBJ<__k>< q1^{0}: PRIM^{1}, q2^{1}: PRIM^{2}, *^{0}: PRIM^{0}>^{0}
Property Assign - 2 o1[y @ {p1}] = o2[x @ {q2, q1}]; x: PRIM^{0} y: PRIM^{0} o1: OBJ<__k>< p1^{2}: PRIM^{3}, p2^{0}: PRIM^{0}, *^{0}: PRIM^{1}>^{0} o2: OBJ<__k>< q1^{0}: PRIM^{1}, q2^{1}: PRIM^{2}, *^{0}: PRIM^{0}>^{0}
Property Assign - 3 o1[y @ {p2}] = o2[x @ {a2, q1}]; x: PRIM^{0} y: PRIM^{0} o1: OBJ<__k>< p1^{2}: PRIM^{3}, p2^{0}: PRIM^{0}, *^{0}: PRIM^{1}>^{0} o2: OBJ<__k>< q1^{0}: PRIM^{1}, q2^{1}: PRIM^{2}, *^{0}: PRIM^{0}>^{0}
Delete Expression - 1 delete o[y]; y: PRIM^{0} o: OBJ<__k>< p1^{2}: PRIM^{3}, p2^{0}: PRIM^{0}, *^{0}: PRIM^{1}>^{0}
Delete Expression - 2 delete o[y]; y: PRIM^{1} o: OBJ<__k>< p1^{2}: PRIM^{3}, p2^{0}: PRIM^{0}, *^{0}: PRIM^{1}>^{0}
Delete Expression - 3 delete o[y @ {p2}]; y: PRIM^{1} o: OBJ<__k>< p1^{2}: PRIM^{3}, p2^{0}: PRIM^{0}, *^{0}: PRIM^{1}>^{0}
If - 1 if (h) { l = 5 } l: PRIM^{0} h: PRIM^{5}
If - 2 if (h) { h = h + 1 } else { h = h - l} l: PRIM^{0} h: PRIM^{5}
If - 3 if (o[y]) { l = 0 } l: PRIM^{0} y: PRIM^{0} o: OBJ<__k>< p1^{0}: PRIM^{3}, p2^{0}: PRIM^{2}, *^{0}: PRIM^{0}>^{0}
If - 4 if (o[y @ {p1}]) { l = 0 } l: PRIM^{0} y: PRIM^{0} o: OBJ<__k>< p1^{0}: PRIM^{3}, p2^{0}: PRIM^{2}, *^{0}: PRIM^{0}>^{0}
If - 5 if (o1[y]) { o2[x] = 0; } x: PRIM^{0} y: PRIM^{0} o1: OBJ<__k>< p1^{2}: PRIM^{3}, p2^{0}: PRIM^{0}, *^{0}: PRIM^{1}>^{0} o2: OBJ<__k>< q1^{0}: PRIM^{1}, q2^{1}: PRIM^{2}, *^{0}: PRIM^{0}>^{0}
While - 1 l = input; while (input > 0) { input = input - 1; l = l*input; } l: PRIM^{0} input: PRIM^{0}
While - 2 l = input; while (input > 0) { input = input - 1; l = l*input; } l: PRIM^{0} input: PRIM^{2}
While - 3 h = input; while (input > 0) { input = input - 1; h = h*input; } h: PRIM^{2} input: PRIM^{0}
While - 4 h = input; while (input > 0) { input = input - 1; h = h*input; } h: PRIM^{2} input: PRIM^{2}
Funcall - 1 h = f(3); h: PRIM^{5} f: FUN<GLOB.(PRIM^{0})->^{0} PRIM^{5}>^{0}
Funcall - 2 l = f(3); l: PRIM^{0} f: FUN<GLOB.(PRIM^{0})->^{0} PRIM^{5}>^{0}
Funcall - 3 l = f(3); l: PRIM^{0} f: FUN<GLOB.(PRIM^{0})->^{0} PRIM^{5}>^{0}
Funcall - 4 l = f(3); l: PRIM^{0} f: FUN<**o1.(PRIM^{0})->^{0} PRIM^{5}>^{0} **o1: OBJ<__k>< p1^{2}: PRIM^{3}, p2^{0}: PRIM^{0}, *^{0}: PRIM^{1}>^{0}
Method Call - 1 l = o['q'](4); l: PRIM^{0} o: **o1 **o1: OBJ<__k><p^{2}: PRIM^{3}, q^{0}: FUN<__k.(PRIM^{3}) ->^{2} PRIM^{3}>^{0}>^{0}
Method Call - 2 h = o['q'](4); h: PRIM^{3} o: **o1 **o1: OBJ<__k><p^{2}: PRIM^{3}, q^{0}: FUN<__k.(PRIM^{3}) ->^{2} PRIM^{3}>^{0}>^{0}
Method Call - 3 if (h) { o['q'](4); } h: PRIM^{3} o: **o1 **o1: OBJ<__k><p^{2}: PRIM^{3}, q^{0}: FUN<__k.(PRIM^{3}) ->^{2} PRIM^{3}>^{0}>^{0}
This - 1 o['q'] = function (x) { h = this['p']; return h; } h: PRIM^{3} o: **o1 **o1: OBJ<__k><p^{2}: PRIM^{3}, q^{0}: FUN<__k.(PRIM^{3}) ->^{2} PRIM^{3}>^{0}>^{0}
This - 2 o['q'] = function (x) { l = this['p']; return h; } l: PRIM^{0} h: PRIM^{3} o: **o1 **o1: OBJ<__k><p^{2}: PRIM^{3}, q^{0}: FUN<__k.(PRIM^{3}) ->^{0} PRIM^{3}>^{0}>^{0}
Function Literal - 1 f = function (x) { return l;}; l: PRIM^{0} f: FUN<GLOB.(PRIM^{0})->^{0} PRIM^{2}>^{0}
Function Literal - 2 f = function (x) { return h;}; h: PRIM^{4} f: FUN<GLOB.(PRIM^{0})->^{0} PRIM^{2}>^{0}
Function Literal - 3 f = function (x) { l = 0; return h;}; l: PRIM^{0} h: PRIM^{3} f: FUN<GLOB.(PRIM^{0})->^{3} PRIM^{3}>^{0}
Function Literal - 4 o['q'] = function (x) { return h; } h: PRIM^{3} o: **o1 **o1: OBJ<__k><p^{2}: PRIM^{3}, q^{0}: FUN<__k.(PRIM^{3}) ->^{2} PRIM^{2}>^{0}>^{0}
Function Literal - 5 o['q'] = function (x) { return l; } l: PRIM^{0} o: **o1 **o1: OBJ<__k><p^{2}: PRIM^{3}, q^{0}: FUN<__k.(PRIM^{3}) ->^{0} PRIM^{0}>^{0}>^{0}
Function Literal - 1 f = l ? function (x) { return 0; } : function (y) { return 1; }; l: PRIM^{0} h: PRIM^{3} f: FUN<GLOB.(PRIM^{0})->^{0} PRIM^{0}>^{0}
Function Literal - 2 f = l ? function (x) { return h; } : function (y) { return 1; }; l: PRIM^{0} h: PRIM^{3} f: FUN<GLOB.(PRIM^{0})->^{0} PRIM^{0}>^{0}
CM = {}; CM.proto_contact = {}; CM.contact_list = {}; CM.proto_contact.printContact = function() { return this.lst + "," + this.fst; }; CM.proto_contact.makeFavorite = function() { this.favorite = null; }; CM.proto_contact.unFavorite = function() { return "favorite" in this ? delete this.favorite : true; }; CM.proto_contact.isFavorite = function() { return "favorite" in this; }; CM.createContact = function(fst_name, lst_name, email) { var contact; contact = {}; contact.__proto__ = CM.proto_contact; contact.fst = fst_name; contact.lst = lst_name; contact.email = email; return contact; }; CM.storeContact = function(contact, i) { var list, key; list = this.contact_list; key = contact.lst+i; if (key in list) { CM.storeContact(contact, i+1); } else { list[key] = contact; } }; CM.getContact = function(lst_name, i) { return this.contact_list[lst_name+i]; };
Global Variable  
Edit Type
Global Variable:  
Security Type:
Type Name  
Edit Type
Type Name:  
Security Type: