TS*: Gradual Typing Embedded Securely in JavaScript

This tutorial accompanies the following paper: Gradual Typing Embedded Securely in JavaScript. For a short, informal overview of TS*, see this slide deck.

A first example

The syntax of TS* is a subset of TypeScript's (itself a superset of JavaScript). TS* programs are a sequence of modules, each containing a sequence of statements (e.g., function or var declarations). Here's factorial programmed in TS*.

module Factorial {
  function factorial(n:number) {
    if (n === 0) { return 1; }
    else { return n * (factorial (n - 1));  }
  }
}

And then call into TS* from your HTML5 web page, which you can build below. Hit the "compile and load" button, and we'll generate JavaScript from TS*, link it with your web page and load everything in the frame to the right.
Enter the body of your HTML5 web page here:

<script type="text/javascript">
function doit() {
   var e = document.getElementById("number"); 
   var n = e.value;
   var f = Factorial.factorial(n);
   var out = document.getElementById("output");
   out.innerText = "Factorial of " + n + " is " + f;
}
</script>
<input id="number" type="text"/>
<input type="submit" value="Compute the factorial!" onclick="doit()"/>
<div id="output"></div>

interface Un { }
interface unit { }
declare function String_at(s: string, index: number): string;
declare function String_concat(s1: string, s2: string): string;
declare function toNumber(s: string): number;
declare function String_fromCharCode(n: number): string;
declare function parseInt(s: string, radix: number): number;
declare function write(o: any, k: any, v: any) : any;
declare function read(o: any, k: any): any;
declare function lengthArray(a: any[]): number;
declare function emptyRecord(x: any): any;
declare function newArray(x: any): any;
declare function JSONStringify(x: any): string;
declare function readArray(x: any, n: number): any;
declare function clearArray(x: any): any;
declare function alert(x: any): any;
declare function localStorage_getItem(k: string): string;
declare function localStorage_setItem(k: string, v: string) : any;
declare function localStorage_hasItem(k: string): bool;
declare function localStorage_clear(x: any) : any;
declare function display_ad(x: Un) : Un;
declare function show (x:Un) : Un;

JSON parsing in TS*

Our next example programs a JSON parser in TS*. There are two points to emphasize about this parser:

The parser is programmed in idiomatic JavaScript, but is easily gradually typed in TS*.
Validating the structure of a parsed JSON object is easy. Instead of verbose and brittle approaches to JSON validation like JSON Schema, TS* allows the programmer to easily express and check properties of objects using types. In particular, the TS* runtime provides a function "Prims.setTag<T>(x:any) : T". Give this function any argument "x", and a desired type for it "T", and it checks that "x" can be given the type "T" and returns it back to you for use as a statically typed "T". (Note: the web IDE we're using here doesn't recognize this TS* feature yet, so you'll see "red squigglies" under every usage of it below, even though it is perfectly legal.)

  module Parser {
    function spaces(s: string, index: number): number {
        if (String_at(s, index) === " ") {
            return spaces(s, index + 1);
        } else {
            return index;
        }
    }
    function isDigit(s) {
        return (s === "0") || (s === "1") || (s === "2") || (s === "3") || (s === "4") || (s === "5") ||
            (s === "6") || (s === "7") || (s === "8") || (s === "9");
    }

    function beginNumber(s) {
        return (s === "-") || (isDigit(s)) || (s === ".");
    }

    function isNumeral(s: string) {
        return isDigit(s) || (s === "+") || (s === "-") || (s === "e") || (s === "E") || (s === ".");
    }

    export function parseNumber(s: string, index: number, accum: string): { fst: number; snd: number; } {
        if (isNumeral(String_at(s, index))) {
            return parseNumber(s, index + 1, String_concat(accum, String_at(s, index)));
        } else {
            return { fst: toNumber(accum), snd: index };
        }
    }

    function parseUnicode(s: string, index: number, ctr: number, accum: number): { fst: string; snd: number; } {
        if (ctr === 3) {
            return { fst: String_fromCharCode(accum), snd: index };
        } else {
            parseUnicode(s, index + 1, ctr + 1, accum * 16 + (parseInt(String_at(s, index), 16)));
        }
    }

    function parseEscapeSequence(s: string, index: number, accum: string): { fst: string; snd: number; } {
        var c = String_at(s, index);
        if (c === "n") {
            return { fst: "\\n", snd: index + 1 };
        } else if (c === "b") {
            return { fst: "\\b", snd: index + 1 };
        } else if (c === "r") {
            return { fst: "\\r", snd: index + 1 };
        } else if (c === "t") {
            return { fst: "\\t", snd: index + 1 };
        } else if (c === "u") {
            return parseUnicode(s, index + 1, 0, 0);
        } else {
            return { fst: "", snd: index }
        }
    }

    function parseString(s: string, index: number, accum: string): { fst: string; snd: number; } {
        if (String_at(s, index) === "\\\"") {
            return { fst: accum, snd: index + 1 };
        } else if (String_at(s, index) === "\\\\") {
            var o = parseEscapeSequence(s, index + 1, "");
            var s1 = o.fst;
            var i1 = o.snd;
            return parseString(s, i1, String_concat(accum, s1));
        } else {
            parseString(s, index + 1, String_concat(accum, String_at(s, index)));
        }
    }

    function parseBool(s: string, i: number): { fst: bool; snd: number; } {
        if ((String_at(s, i) === "t") && (String_at(s, i + 1) === "r") && (String_at(s, i + 2) === "u") &&
            (String_at(s, i + 3) === "e")) {
            return { fst: true, snd: i + 4 };
        } else if ((String_at(s, i) === "f") && (String_at(s, i + 1) === "a") &&
            (String_at(s, i + 2) === "l") && (String_at(s, i + 3) === "s") &&
            (String_at(s, i + 4) === "e")) {
            return { fst: false, snd: i + 5 };
        } else {
            return { fst: true, snd: i + 4 };
        }
    }

    function addField(o: any, k: string, v: any) {
        if (k === "rtti") {
            return undefined;
        } else {
            write(o, k, v);
            return undefined;
        }
    }

    function parseArray(s: string, i: number, a: any[]): { fst: any[]; snd: number; } {
        var i1 = spaces(s, i);
        if (String_at(s, i1) === "]") {
            return { fst: a, snd: i1 + 1 };
        } else {
            var o = parseValue(s, i1);
            var v = o.fst;
            var i2 = o.snd;
            write(a, (lengthArray(a)), v);
            var i3 = spaces(s, i2);
            if (String_at(s, i3) === ",") {
                parseArray(s, i3 + 1, a);
            } else {
                parseArray(s, i3, a);
            }
        }
    }

    function parseObject(s: string, i: number, o: any): { fst: any; snd: number; } {
        var i1 = spaces(s, i);
       
        if (String_at(s, i1) === "}") {
            return { fst: o, snd: i1 + 1 };
        } else {
            var o1 = parseString(s, i1 + 1, "");
            var key = o1.fst;
            var i2 = o1.snd;
            var i3tmp = spaces(s, i2);
            var i3 = spaces(s, i3tmp + 1);
            var o2 = parseValue(s, i3);
            var value = o2.fst; 

            var i4 = o2.snd;
            addField(o, key, value);
            var i5 = spaces(s, i4);
            if (String_at(s, i5) === ",") {
                parseObject(s, i5 + 1, o);
            } else {
                parseObject(s, i5, o);
            }
        }
    }

    function parseValue(s: string, i: number): { fst: any; snd: number; } {
        var i1 = spaces(s, i);
        if (String_at(s, i1) === "\\\"") {
            return parseString(s, i1 + 1, "");
        } else if ((String_at(s, i1) === "t") || (String_at(s, i1) === "f")) {
            return parseBool(s, i1);
        } else if (beginNumber(String_at(s, i1))) {
            return parseNumber(s, i1, "");
        } else if (String_at(s, i1) === "{") {
            return parseObject(s, i1 + 1, emptyRecord(undefined));
        } else if (String_at(s, i1) === "[") {
            return parseArray(s, i1 + 1, []);
        } else {
            return parseString(s, i1 + 1, "");
        }
    }

    export function parse(s: string): any {
        return parseValue(s, 0).fst;
    }

    export function check(o:any) : {hello:string;} {
       return Prims.setTag<{ hello : string;}>(o);
    }
}

Here's a bit of HTML code to drive the parser. It lets you enter a JSON string in a text box, parses it, checks that it has type {hello:string} and then prints it back to you.

<script type="text/javascript">
function parseit() {
   var s = document.getElementById("jsonstring").value;
   var o = Parser.check(Parser.parse(s));
   alert("You said hello " + o.hello);
}
</script>
<input id="jsonstring" type="text"/>
<input type="submit" value="Parse JSON" onclick="parseit()"/>

Secure local storage

Our last example combines the JSON parser with a local storage API. See the slide deck for a high-level view of what this code does. Briefly, we demonstrate how to write a wrapper around HTML5 local storage that provides a high-integrity cache of a typed view of the store. For this demo, we view the store as containing two fragments, each holding values at a different types. These are the "Players" and "Games" fragments below.
We also illustrate an extremely simply authorization scheme which requires a caller to present a token to access the store API. Our paper shows how such tokens can be embedded securely inside scripts, even in the presence of XSS attacks. We'll soon integrate that here.
Finally, we show how the store remains resilient to attacks mounted from arbitrary JavaScript. Towards the end, we show various JavaScript attackers, including a "bazooka" attacker that attempts to corrupt all the base objects in JavaScript---still, TS*'s type safety cannot be subverted.
These examples illustrate the use of TS*'s "Un" type, which models untrusted adversarial code. The only way to manipulate these values safely inside TS* is via the use of "Prims.wrap<T,U>(x:T) : U". As with setTag previously, this function is supported by the TS* runtime (but is not yet recognized by the IDE we're using here).

module StorageLib {
    
    // helper function to initialize players cache
    function initPlayers(players: { pname: string; profile: { car: string; score: number;
                                                              otherinfo: any; };
                                  }[], i: number, n: number)
                                  
    {
        if (i === n) {
            return undefined;
        } else {
            var key = String_concat("p", JSONStringify(i));
            var value = Parser.parse(localStorage_getItem(key));
            write(players, i, value);
            return initPlayers(players, i + 1, n);
        }
    }

    // helper function to initialize games cache
    function initGames(games: { gname: string; state: { pname: string; position: number;
                                                        dead: bool; }[];
                              }[], i: number, n: number)
    {
        if (i === n) {
            return undefined;
        } else {
            var key = String_concat("g", JSONStringify(i));
            var value = Parser.parse(localStorage_getItem(key));
            write(games, i, value);
            return initGames(games, i + 1, n);
        }
    }

    // helper function to commit players cache
    function commitPlayers(players: { pname: string; profile: { car: string; score: number;
                                                                otherinfo: any; };
                                    }[], i: number)
    {
        if (i === lengthArray(players)) {
            return localStorage_setItem("numPlayers",
                                              JSONStringify(lengthArray(players)));
        } else {
            var key = String_concat("p", JSONStringify(i));
            var value = JSONStringify(readArray(players, i));
            localStorage_setItem(key, value);
            return commitPlayers(players, i + 1);
        }
    }

    // helper function to commit games cache
    function commitGames(games: { gname: string; state: { pname: string; position: number;
                                                          dead: bool; }[];
                                }[], i: number)
    {
        if (i === lengthArray(games)) {
            return localStorage_setItem("numGames",
                                              JSONStringify(lengthArray(games)));
        } else {
            var key = String_concat("g", JSONStringify(i));
            var value = JSONStringify(readArray(games, i));
            localStorage_setItem(key, value);
            return commitGames(games, i + 1);
        }
    }

    function mkInitStorage (x: any) : {
        addItem(token: string, table: string, v: any): number;
        getItem(token: string, table: string, i: number): any;
        commit(token: string): bool;
        clear(token: string): bool;
    }
    {
        // in memory caches for players and games
        var players: {pname: string; profile: {car: string; score: number; otherinfo: any;};}[] = [];
        var games: {gname: string; state: {pname: string; position: number; dead: bool;}[];}[] = [];

        // initialize players cache
        var numPlayers = { v: 0 };
        if (localStorage_hasItem("numPlayers")) {
            var o = Parser.parseNumber(localStorage_getItem("numPlayers"), 0, "");
            numPlayers.v = o.snd;
        }
        initPlayers(players, 0, numPlayers.v);

        // initialize games cache
        var numGames = { v: 0 };
        if (localStorage_hasItem("numGames")) {
            var o = Parser.parseNumber(localStorage_getItem("numGames"), 0, "");
            numGames.v = o.snd;
        }
        initGames(games, 0, numGames.v);

        // addItem helper
        // NOTE: No validation code !
        var addItem = function (table: string, v: any): number {
            if (table === "Player") {
                var n = write(players, lengthArray(players), v);

                // interaction with third-party ad library
                Prims.wrap<(Un) => Un, (any) => unit>(display_ad)(v.profile.car);

                // interaction with UI application code
                Prims.wrap<(Un) => Un, (any) => unit>(show)(v);

                return n; 
            } else if (table === "Game") {
                var n1 = write(games, lengthArray(games), v);
                Prims.wrap<(Un) => Un, (any) => unit> (show)(v); 
                return n1;
            } else {
                return 0;
            }
        };

        // query cacehe functionality
        var getItem = function (table: string, index: number): any {
            if (table === "Player") {
                return read(players, index);
            } else if (table === "Game") {
                return read(games, index);
            } else {
                return undefined;
            }
        };

        var commit = function (x: any): bool {
            commitPlayers(players, 0);
            commitGames(games, 0);
            return true;
        }

        var clear = function (x: any): bool {
            clearArray(players);
            clearArray(games);
            localStorage_clear(undefined);
            return true;
        }

        // obtained using XMLHttpRequest, for example
        var auth = "auth1234";

        return {
            addItem: function (token: string, table: string, v: any) {
                if (token === auth) {
                    return addItem(table, v);
                } else {
                    return 0;
                }
            },
            getItem: function (token: string, table: string, index: number) {
                if (token === auth) {
                    return getItem(table, index);
                } else {
                    return undefined;
                }
            },
            commit: function (token: string) {
                if (token === auth) {
                    return commit(undefined);
                } else {
                    return false;
                }
            },
            clear: function (token: string) {
                if (token === auth) {
                    return clear(undefined);
                } else {
                    return false;
                }
            }
        };
    }
    var initStorage = mkInitStorage(0);

    export function user_a (x:unit) : any
    {
        // trying to add an ill-formed record, profile fields missing
        alert("User A");
        initStorage.addItem("auth1234", "Player", {pname:"p1", profile:{car:"bmw"}});
    }

    export function user_b (x: unit) : any
    {
        initStorage.addItem("auth1234", "Player", { pname: "p1", profile: { car: "ferrari", score: 200, otherinfo: true } });
        var o = initStorage.getItem("auth1234", "Player", 0);

        // try to corrupt the cache
        alert("User B: Trying to corrupt the cache");
        o["pname"] = 1;
        alert("Player name in the cache is");
        alert(o.pname);
    }

    export function user_c(x: unit): any
    {
        initStorage.addItem("auth1234", "Player", { pname: "p1", profile: { car: "ferrari", score: 200, otherinfo: true } });
        var o = initStorage.getItem("auth1234", "Player", 0);

        // see if cache has been corrupted by show functionality
        alert("User C: Player name in the cache is");
        alert(o.pname);
    }

    export function user_d(x: unit): any
    {
        // stack walk test case
        alert("User D: Trying to steal token ...");
        initStorage.addItem("auth1234", "Player", { pname: "p1", profile: { car: "ferrari", score: 200, otherinfo: true } });
    }
}

Here's a top-level from JavaScript that attempts to corrupt the store using various tricks, e.g., stack walking, prototype poisoning etc. Look at the source of the included JavaScript files below (especially bazooka.js) to see the extent of the attacks we're coping with. In each case, any attempt to corrupt the database or steal an authorization token will be detected and prevented. For the purposes of the demo, we raise these type checking errors as exceptions which can be caught and suppressed. For a real deployment, these errors can be made fatal, if so desired.

<script src="/Tools/FStar/lib/ui.js"></script>
<script src="/Tools/FStar/lib/ad.js"></script>
<script src="/Tools/FStar/lib/bazooka.js"></script>
<script type="text/javascript">
try { StorageLib.user_a(); }
catch (err) {}

try { StorageLib.user_b(); }
catch (err) {}

try { StorageLib.user_c(); }
catch (err) {}

try { StorageLib.user_d(); }
catch (err) {}
</script>

TS*: Gradual Typing Embedded Securely in JavaScript

A first example

JSON parsing in TS*

Secure local storage

tutorials