Linvail

Linvail is npm module that implements a control access system around JavaScript code instrumented by Aran. Linvail's motivation is to build dynamic analyses capable of tracking primitive values across the object graph.

Getting Started

npm install acorn aran astring linvail 

const Acorn = require("acorn");
const Aran = require("aran");
const Astring = require("astring");
const Linvail = require("linvail");

const aran = Aran({namespace:"META", sandbox:true});
const instrument = (script, parent) =>
  Astring.generate(aran.weave(Acorn.parse(script), pointcut, parent));
let counter = 0;
const linvail = Linvail({
  instrument: instrument,
  enter: (value) => ({base:value, meta:"#"+(counter++)}),
  leave: (value) => value.base
});
const pointcut = Object.keys(linvail.advice);

global.META = Object.assign({}, linvail.advice);
global.META.primitive = (primitive, serial) => {
  const result = linvail.advice.primitive(primitive, serial);
  console.log(result.meta+"("+result.base+") // @"+serial);
  return result;
};
global.META.binary = (operator, left, right, serial) => {
  const result = linvail.advice.binary(operator, left, right, serial);
  console.log(result.meta+"("+result.base+") = "+left.meta+" "+operator+" "+right.meta+" // @"+serial);
  return result;
};

global.eval(Astring.generate(aran.setup()));
global.eval(instrument(`
let division = {};
division.dividend = 1 - 1;
division.divisor = 20 - 2 * 10;
division.result = division.dividend / division.divisor;
if (isNaN(division.result))
  console.log("!!!NaN division result!!!");
`));

#6(apply) // @2
#10(defineProperty) // @2
#14(getPrototypeOf) // @2
#18(keys) // @2
#22(iterator) // @2
#24(undefined) // @2
#26(dividend) // @6
#27(1) // @9
#28(1) // @10
#29(0) = #27 - #28 // @8
#30(divisor) // @12
#31(20) // @15
#32(2) // @17
#33(10) // @18
#34(20) = #32 * #33 // @16
#35(0) = #31 - #34 // @14
#36(result) // @20
#37(dividend) // @23
#38(divisor) // @25
#39(NaN) = #29 / #35 // @22
#42(result) // @30
#45(log) // @33
#46(!!!NaN division result!!!) // @35
!!!NaN division result!!!

Demonstrators

• demo/analysis/identity-explicit.js Demonstrate the API of linvail but don't produce any observable effect.
• demo/analysis/identity: Same as above but uses the simplified live API of Aran.
• demo/analysis/wrapper: Every values entering instrumented areas are wrapped to provide a well-defined identity. Every wrapper leaving instrumented areas are unwrapped so the behavior of the base program is not altered. Wrapping and unwrapping operations are logged.
• demo/analysis/concolic: Same as above but also logs the arguments and result of triggered aran's traps. The resulting log is a detailed data-flow trace which with proper formating can be fed to a SMT solver.

API

• A base value is either:
  • a primitive
  • a reference which satisfies the below constraints:
    • its prototype is a base value
    • the values of its data properties are base values
    • the getters and setters of its accessor properties are base values
    • applying it with a base value this-argument and base value arguments will return a base value
    • constructing it with base value arguments will return a base value
• A meta value is either:
  • a primitive
  • a reference which satisfies the below constraints:
    • its prototype is a meta value.
    • the values of its data properties are inner values
    • the getters and setters of its accessor properties are meta values
    • applying it with a meta value this-argument and inner value arguments will return an inner value
    • constructing it with base value arguments will return an inner value

linvail = require("linvail")(membrane)

• membrane :: object
  • inner = membrane.enter(meta): User-defined function to convert a meta value to an inner value.
  • meta = membrane.leave(inner): User-defined function to convert an inner value to a meta value.
  • instrumented = membrane.instrument(code, serial): This function will be called to transforms code before passing it to the infamous eval function.
    • code :: string
    • serial :: number
    • instrumented :: string
• linvail :: object
  • linvail.advice :: object An aran advice, contains Aran traps and a SANDBOX field which is set to linvail.metaof(global). The actual traps triggered by Aran can
  • linvail.membrane :: object: The same object as the membrane arguments.
  • base = linvail.baseof(meta): Convert a meta value into a base value.
  • meta = linvail.metaof(base) Convert a base value into a meta value.

Discussion

Aran and program instrumentation in general is good for introspecting the control flow and pointers data flow. Things become more difficult when reasoning about primitive value data flow is involved. For instance, there is no way at the JavaScript language level to differentiate two null values even though they have different origins. This restriction strikes every JavaScript primitive values because they are inlined into different parts of the program's state -- e.g the environment and the value stack. All of these copying blur the concept of a primitive value's identity and lifetime. By opposition, objects can be properly differentiated based on their address in the store. Such situation happens in almost every mainstream programming languages. We now discuss several strategies to provide an identity to primitive values:

• Shadow States: For low-level languages such as binary code, primitive values are often tracked by maintaining a so called "shadow state" that mirrors the concrete program state. This shadow state contains analysis-related information about the program values situated at the same location in the concrete state. Valgrind is a popular binary instrumentation framework which utilizes this technique to enables many data-flow analyses. The difficulty of this technique lies in maintaining the shadow state as non-instrumented functions are being executed. In JavaScript this problem typically arises when objects are passed to non instrumented functions such as builtins. Keeping the shadow store in sync during such operation requires to know the exact semantic of the non-instrumented function. Since they are so many different builtin functions in JavaScript, this is a very hard thing to do.
• Record And Replay: Record and replay systems such as Jalangi are an intelligent response to the challenge of keeping in sync the shadow state with its concrete state. Acknowledging that divergences between shadow and concrete states cannot be completely avoided, these systems allows divergences in the replay phase which can be recovered from by utilizing the trace gathered during the record phase. We propose two arguments against such technique: First, every time divergences are resolved in the replay phase, values with unknown origin are being introduced which necessarily diminish the precision of the resulting analysis. Second, the replay phase only provide information about partial execution which can be puzzling to reason about.
• Wrappers: Instead of providing an entire separated shadow state, wrappers constitute a finer grained solution. By wrapping primitive values inside objects we can simply let them propagate through the data flow of the base program. The challenge introduced by wrappers is to make them behave like their wrapped primitive value to non-instrumented code. We explore three solutions to this challenge:
  • Boxed Values: JavaScript enables to box booleans, numbers and strings. Despite that symbols, undefined and null cannot be tracked by this method, boxed values do not always behave like their primitive counterpart within builtins.

    // Strings cannot be differentiated based on their origin
    let string1 = "abc";
    let string2 = "abc";
    assert(string1 === string2);
    // Boxed strings can be differentiated based on their origin
    let boxed_string1 = new String("abc");
    let boxed_string2 = new String("abc");
    assert(boxed_string1 !== boxed_string2);
    // Boxed value behave as primitive in some builtins: 
    assert(JSON.stringify({a:string1}) === JSON.stringify({a:boxed_string1}));
    // In others, they don't...
    let error
    try {
      Object.defineProperty(string1, "foo", {value:"bar"});
    } catch (e) {
      error = e;
    }
    assert(error);
    Object.defineProperty(boxed_string1, "foo", {value:"bar"});

  • valueOf Method: A similar mechanism to boxed value is to use the valueOf method. Many JavaScript builtins expecting a primitive value but receiving an object will try to convert this object into a primitive using its valueOf method. As for boxed values this solution is not bullet proof and there exists many cases where the valueOf method will not be invoked.
  • Explicit Wrappers: Finally a last options consists in using explicit wrappers which should be cleaned up before escaping to non-instrumented code. This requires to setup an access control system between instrumented code and non-instrumented code. This the solution that Linvail directly enables.

Acknowledgments

I'm Laurent Christophe a phd student at the Vrij Universiteit of Brussel (VUB). I'm working at the SOFT language lab in close relation with my promoters Coen De Roover and Wolfgang De Meuter. I'm currently being employed on the Tearless project.