Merge Private Master Branch Commits into Public Repo

.gitignore

@@ -22,6 +22,12 @@ report
 /test_reports/*
 
 *~
+*#
 
 trace.log
 /coq/#JsPrettyRules.v#
+
+.tern-port
+
+proof.patched
+

.gitlab-ci.yml

@@ -0,0 +1,13 @@
+stages:
+  - test
+  - Git Sync
+
+git-sync:
+  stage: Git Sync
+  script:
+  - eval `ssh-agent`
+  - echo "$PUSH_KEY" | ssh-add -
+  - git sync-remote [email protected]:resource-reasoning/jscert_dev.git [email protected]:resource-reasoning/jscert_dev.git
+  - ssh-agent -k
+  only:
+  - triggers

.gitmodules

@@ -1,6 +1,6 @@
 [submodule "interp/parser"]
 	path = interp/parser
-	url = https://github.com/resource-reasoning/JS_Parser.git
+	url = http://github.com/resource-reasoning/JS_Parser.git
 [submodule "lib/tlc"]
 	path = lib/tlc
 	url = https://gforge.inria.fr/git/tlc/tlc.git

Makefile

@@ -123,7 +123,7 @@ tags: $(JS_SRC)
 .PHONY: install_depend install_optional_depend
 install_depend:
 	# Install coq if required
-	if ! which $(COQC); then opam install -y coq; fi
+	if ! which $(COQC); then opam pin add coq 8.4.6; opam install -y coq; fi
 	opam install -y xml-light ocamlfind yojson
 
 install_optional_depend: install_depend
@@ -271,22 +271,6 @@ interp/run_jsbisect.native: interp/src/extract/JsInterpreterBisect.ml
 
 # interp/run_jsbisect is an implicit rule
 
-#######################################################
-# Tracing version of the interpreter
-
-interp/tracer/annotml/ppx_lines.native:
-	$(MAKE) -C interp/tracer/annotml ppx_lines.native
-
-interp/src/extract/JsInterpreterTrace.ml: interp/src/extract/JsInterpreter.ml extract_interpreter
-	cp $< $@
-
-interp/src/run_jstrace.ml: interp/src/run_js.ml
-	perl -pe 's/JsInterpreter\./JsInterpreterTrace\./g' $< > $@
-
-interp/run_jstrace.native: interp/src/extract/JsInterpreterTrace.ml interp/tracer/annotml/ppx_lines.native
-
-# interp/run_jstrace is an implicit rule
-
 #######################################################
 # Interpreter run helpers
 .PHONY: run_tests run_tests_spidermonkey run_tests_lambdaS5 run_tests_nodejs
@@ -314,7 +298,6 @@ clean_interp:
 	-rm -f interp/run_jsbisect interp/src/run_jsbisect.ml
 	-rm -f interp/run_jstrace interp/src/run_jstrace.ml
 	cd interp && $(OCAMLBUILD) -quiet -clean
-	$(MAKE) -C interp/tracer/annotml clean
 
 clean: clean_interp
 	-rm -f coq/*.{vo,glob,d}

README.org

@@ -18,7 +18,7 @@
     You can get the latest source from [[https://github.com/jscert/jscert][here]].
 
     JSCert depends on:
-    - Coq
+    - Coq (version 8.4.6)
 	- OCaml (version 4 or above minimum, 4.02 or above for all optional features to build)
     - Java (for the parser)
 

com/2016_04_27_certif.txt

@@ -0,0 +1,59 @@
+
+@erights, all,
+
+I discussed with Alan and here are a few answers/comments.
+
+*) I did tell you that, to establish a security theorem, you need to
+formalize all the "features" of the language. As Dominique 
+pointed out, for many libraries, which are written in pure JS 
+(or at least are morally equivalent to pure JS code), we don't need
+to formalize them, because such libraries don't introduce additional
+"language features" which might give rise to security breaches. 
+However, any library that has an internal state (e.g. Date, Random, 
+and I suppose many interactions with the DOM, etc..) can be potential 
+sources of trouble. Indeed, as soon as a stateful module might get 
+called both by trusted code and untrusted code, you may have 
+an information channel that might be exploited.
+
+*) We agree that it is somewhat unrealistic to expect all language
+features to be formalized before starting to work on the proof
+of security theorems. Like you said, we should attempt to work out 
+and to formally state in Coq the invariants that are required for
+proving the theorems of interest. Then, we could advertise these
+invariants (translated in English prose) to the developers of the
+various language features, in the hope that those developers can
+confirm that their features indeed satisfy the invariants---or 
+at least that they intend to.
+
+*) Regarding the statement of the invariants, we should work on them
+together. In particular, Alan and I came up with some ideas for
+specifying what a proxy should guarantee. We should discuss that
+with you, probably offline (we expect a certain number of iterations 
+may be needed to converge to something that makes enough sense).
+In general, to formally express particular invariants, it is required
+to augment the semantics with so-called "ghost" information, used
+for keeping track, e.g., of the set of pointers that have been 
+leaked on purpose.
+
+*) In parallel, we believe it would still be worthwhile extending our 
+reference interpreter from ES5 to a large subset of ES6. However,
+we simply don't have the manpower to do this work ourselves. 
+Nevertheless, we would be happy to help whenever a difficulty is 
+encountered. Note that our interpreter is currently written in a 
+tiny subset of the OCaml language. Overall, we believe it should 
+not be hard for a programmer with no experience in OCaml to extend our interpreter.
+
+---Remark: our interpreter used to be written in Coq and extracted 
+to OCaml but we cound it simpler to write OCaml directly; we are 
+looking forward to generate Coq definitions from OCaml code in the 
+future. We were even tempted to consider writing the interpreter 
+a tiny subset of JS, but we found that OCaml provides a far more 
+concise syntax, moreover it provides handy type-checking of the code. 
+In addition, that our OCaml interpreter gets translated to readable 
+and executable JS code.)
+
+(Alan will present the interpreter and give a demo in May.)
+
+
+Best,
+Arthur

coq/.gitignore

@@ -1,2 +1,3 @@
 *~
+.*.aux
 

coq/JsCorrectness.v

@@ -2800,10 +2800,10 @@ Proof.
 Qed.
 
 
-Lemma binding_inst_function_decls_correct : forall runs S C args L fds str bconfig o,
+Lemma binding_inst_function_decls_correct : forall runs S C L fds str bconfig o,
   runs_type_correct runs ->
   binding_inst_function_decls runs S C L fds str bconfig = o ->
-  red_expr S C (spec_binding_inst_function_decls args L fds str bconfig) o.
+  red_expr S C (spec_binding_inst_function_decls L fds str bconfig) o.
 Proof.
   introv IH HR. gen S o. induction fds; introv HR.
   simpls. run_inv. applys* red_spec_binding_inst_function_decls_nil.
@@ -2813,7 +2813,7 @@ Proof.
   let_name as M. rename a into fd. rename l into fo.
   asserts M_correct: (forall S o,
       M S = o ->
-      red_expr S C (spec_binding_inst_function_decls_5 args L fd fds str fo bconfig) o).
+      red_expr S C (spec_binding_inst_function_decls_5 L fd fds str fo bconfig) o).
     clears HR S o. introv HR. subst M.
     subst fname. run red_spec_binding_inst_function_decls_5
       using env_record_set_mutable_binding_correct.
@@ -2981,12 +2981,12 @@ Proof.
     clear EQA. apply~ red_spec_create_arguments_object_4.
 Qed.
 
-Lemma binding_inst_arg_obj_correct : forall runs S C lf p xs args L o,
+Lemma binding_inst_arg_obj_correct : forall runs S C lf str xs args L o,
   runs_type_correct runs ->
-  binding_inst_arg_obj runs S C lf p xs args L = o ->
-  red_expr S C (spec_binding_inst_arg_obj lf p xs args L) o.
+  binding_inst_arg_obj runs S C lf xs args L str = o ->
+  red_expr S C (spec_binding_inst_arg_obj lf xs args L str) o.
 Proof.
-  introv IH HR. unfolds in HR. let_name.
+  introv IH HR. unfolds in HR.
   run~ red_spec_binding_inst_arg_obj using create_arguments_object_correct.
   cases_if.
    run red_spec_binding_inst_arg_obj_1_strict

coq/JsInterpreter.v

@@ -999,82 +999,6 @@ Fixpoint array_args_map_loop runs S C l args ind : result_void :=
   | nil => res_void S
   end.
 
-Definition string_of_prealloc (B : prealloc) : string :=
-match B with
-  | prealloc_global => "global"
-  | prealloc_global_eval => "global_eval"
-  | prealloc_global_parse_int => "global_parse_int"
-  | prealloc_global_parse_float => "global_parse_float"
-  | prealloc_global_is_finite => "global_is_finite"
-  | prealloc_global_is_nan => "global_is_nan"
-  | prealloc_global_decode_uri => "global_decode_uri"
-  | prealloc_global_decode_uri_component => "global_decode_uri_component"
-  | prealloc_global_encode_uri => "global_encode_uri"
-  | prealloc_global_encode_uri_component => "global_encode_uri_component"
-  | prealloc_object => "object"
-  | prealloc_object_get_proto_of => "object_get_proto_of"
-  | prealloc_object_get_own_prop_descriptor => "object_get_own_prop_descriptor"
-  | prealloc_object_get_own_prop_name => "object_get_own_prop_name"
-  | prealloc_object_create => "object_create"
-  | prealloc_object_define_prop => "object_define_prop"
-  | prealloc_object_define_props => "object_define_props"
-  | prealloc_object_seal => "object_seal"
-  | prealloc_object_freeze => "object_freeze"
-  | prealloc_object_prevent_extensions => "object_prevent_extensions"
-  | prealloc_object_is_sealed => "object_is_sealed"
-  | prealloc_object_is_frozen => "object_is_frozen"
-  | prealloc_object_is_extensible => "object_is_extensible"
-  | prealloc_object_keys => "object_keys"
-  | prealloc_object_keys_call => "object_keys_call"
-  | prealloc_object_proto => "object_proto_"
-  | prealloc_object_proto_to_string => "object_proto_to_string"
-  | prealloc_object_proto_value_of => "object_proto_value_of"
-  | prealloc_object_proto_has_own_prop => "object_proto_has_own_prop"
-  | prealloc_object_proto_is_prototype_of => "object_proto_is_prototype_of"
-  | prealloc_object_proto_prop_is_enumerable => "object_proto_prop_is_enumerable"
-  | prealloc_function => "function"
-  | prealloc_function_proto => "function_proto"
-  | prealloc_function_proto_to_string => "function_proto_to_string"
-  | prealloc_function_proto_apply => "function_proto_apply"
-  | prealloc_function_proto_call => "function_proto_call"
-  | prealloc_function_proto_bind => "function_proto_bind"
-  | prealloc_bool => "bool"
-  | prealloc_bool_proto => "bool_proto"
-  | prealloc_bool_proto_to_string => "bool_proto_to_string"
-  | prealloc_bool_proto_value_of => "bool_proto_value_of"
-  | prealloc_number => "number"
-  | prealloc_number_proto => "number_proto"
-  | prealloc_number_proto_to_string => "number_proto_to_string"
-  | prealloc_number_proto_value_of => "number_proto_value_of"
-  | prealloc_number_proto_to_fixed => "number_proto_to_fixed"
-  | prealloc_number_proto_to_exponential => "number_proto_to_exponential"
-  | prealloc_number_proto_to_precision=> "number_proto_to_precision"
-  | prealloc_array => "array"
-  | prealloc_array_is_array => "array_is_array"
-  | prealloc_array_proto => "array_proto"
-  | prealloc_array_proto_to_string => "array_proto_to_string"
-  | prealloc_array_proto_join => "array_proto_join"
-  | prealloc_array_proto_pop => "array_proto_pop"
-  | prealloc_array_proto_push => "array_proto_push"
-  | prealloc_string => "string"
-  | prealloc_string_proto => "string_proto"
-  | prealloc_string_proto_to_string => "string_proto_to_string"
-  | prealloc_string_proto_value_of => "string_proto_value_of"
-  | prealloc_string_proto_char_at => "string_proto_char_at"
-  | prealloc_string_proto_char_code_at=> "string_proto_char_code_at"
-  | prealloc_math => "math"
-  | prealloc_mathop _ => "mathop"
-  | prealloc_date => "date"
-  | prealloc_regexp => "regexp"
-  | prealloc_error => "error"
-  | prealloc_error_proto => "error_proto"
-  | prealloc_native_error _ => "native_error"
-  | prealloc_native_error_proto _ => "native_error_proto"
-  | prealloc_error_proto_to_string => "error_proto_to_string"
-  | prealloc_throw_type_error => "throw_type_error"
-  | prealloc_json => "json"
-end.
-
 Definition run_construct_prealloc runs S C B (args : list value) : result :=
   match B with
 
@@ -1356,16 +1280,15 @@ Definition create_arguments_object runs S C lf xs args X str : result :=
         if_bool (object_define_own_prop runs S2 C l "callee" A false) (fun S3 b' =>
           res_ter S3 l)))).
 
-Definition binding_inst_arg_obj runs S C lf p xs args L : result_void :=
+Definition binding_inst_arg_obj runs S C lf xs args L str : result_void :=
   let arguments := "arguments" in
-  'let str := prog_intro_strictness p in
-    if_object (create_arguments_object runs S C lf xs args
-                   (execution_ctx_variable_env C) str) (fun S1 largs =>
-      if str then
-        if_void (env_record_create_immutable_binding S1 L arguments) (fun S2 =>
-          env_record_initialize_immutable_binding S2 L arguments largs)
-      else
-        env_record_create_set_mutable_binding runs S1 C L arguments None largs false).
+  if_object (create_arguments_object runs S C lf xs args
+                 (execution_ctx_variable_env C) str) (fun S1 largs =>
+    if str then
+      if_void (env_record_create_immutable_binding S1 L arguments) (fun S2 =>
+        env_record_initialize_immutable_binding S2 L arguments largs)
+    else
+      env_record_create_set_mutable_binding runs S1 C L arguments None largs false).
 
 Fixpoint binding_inst_var_decls runs S C L (vds : list string) bconfig str : result_void :=
   match vds with
@@ -1396,7 +1319,7 @@ Definition execution_ctx_binding_inst runs S C (ct : codetype) (funco : option o
             in
           match ct, funco, bdefined with
           | codetype_func, Some func, false =>
-            if_void (binding_inst_arg_obj runs S2 C func p names args L) follow2
+            if_void (binding_inst_arg_obj runs S2 C func names args L str) follow2
           | codetype_func, _, false =>
             impossible_with_heap_because S2 "Weird `arguments' object in [execution_ctx_binding_inst]."
           | _, _, _ => follow2 S2

coq/JsInterpreterExtraction.v

@@ -16,6 +16,11 @@ Require Import ExtrOcamlBasic.
 Require Import ExtrOcamlNatInt.
 Require Import ExtrOcamlString.
 
+(* Do not optimize anything, to make the extracted code simpler to work with *)
+Unset Extraction Optimize.
+Unset Extraction KeepSingleton.
+Unset Extraction AutoInline.
+
 (* Optimal fixpoint. *)
 Extraction Inline FixFun3 FixFun3Mod FixFun4 FixFun4Mod FixFunMod curry3 uncurry3 curry4 uncurry4.
 (* As classical logic statements are now unused, they should not be extracted
@@ -227,16 +232,9 @@ Extract Constant parse_pickable => "(fun s strict ->
 
 
 (* Debugging *)
-Extract Inlined Constant not_yet_implemented_because => "(fun s ->
-  print_endline (__LOC__ ^ "": Not implemented because: "" ^ Prheap.string_of_char_list s) ;
-  Coq_result_not_yet_implemented)".
-Extract Inlined Constant impossible_because => "(fun s ->
-  print_endline (__LOC__ ^ "": Stuck because: "" ^ Prheap.string_of_char_list s) ;
-  Coq_result_impossible)".
-Extract Inlined Constant impossible_with_heap_because => "(fun s message ->
-  print_endline (__LOC__ ^ "": Stuck!\nState:  "" ^ Prheap.prstate true s
-    ^ ""\nMessage:\t"" ^ Prheap.string_of_char_list message) ;
-  Coq_result_impossible)".
+Extract Inlined Constant not_yet_implemented_because => "(fun s -> Debug.not_yet_implemented_because __LOC__ s; Coq_result_not_yet_implemented)".
+Extract Inlined Constant impossible_because => "(fun s -> Debug.impossible_because __LOC__ s; Coq_result_impossible)".
+Extract Inlined Constant impossible_with_heap_because => "(fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)".
 
 
 (* Final Extraction *)

coq/JsPrettyInterm.v

@@ -336,17 +336,17 @@ Inductive ext_expr :=
   | spec_binding_inst_formal_params_2 : list value -> env_loc -> string -> list string -> strictness_flag -> value -> out -> ext_expr
   | spec_binding_inst_formal_params_3 : list value -> env_loc -> string -> list string -> strictness_flag -> value -> ext_expr
   | spec_binding_inst_formal_params_4 : list value -> env_loc -> list string -> strictness_flag -> out -> ext_expr
-  | spec_binding_inst_function_decls :  list value -> env_loc -> list funcdecl -> strictness_flag -> bool -> ext_expr
-  | spec_binding_inst_function_decls_1 : list value -> env_loc -> funcdecl -> list funcdecl -> strictness_flag -> bool -> out -> ext_expr
-  | spec_binding_inst_function_decls_2 : list value -> env_loc -> funcdecl -> list funcdecl -> strictness_flag -> object_loc -> bool -> out -> ext_expr
-  | spec_binding_inst_function_decls_3 : list value -> funcdecl -> list funcdecl -> strictness_flag -> object_loc -> bool -> specret full_descriptor -> ext_expr
-  | spec_binding_inst_function_decls_3a : list value -> funcdecl -> list funcdecl -> strictness_flag -> object_loc -> bool -> full_descriptor -> ext_expr
-  | spec_binding_inst_function_decls_4 : list value -> env_loc -> funcdecl -> list funcdecl -> strictness_flag -> object_loc -> bool -> out -> ext_expr
-  | spec_binding_inst_function_decls_5 : list value -> env_loc -> funcdecl -> list funcdecl -> strictness_flag -> object_loc -> bool -> ext_expr
-  | spec_binding_inst_function_decls_6 : list value -> env_loc -> list funcdecl -> strictness_flag -> bool -> out -> ext_expr
-  | spec_binding_inst_arg_obj :   object_loc -> prog -> list string -> list value -> env_loc -> ext_expr
-  | spec_binding_inst_arg_obj_1 : prog -> env_loc -> strictness_flag -> out -> ext_expr
-  | spec_binding_inst_arg_obj_2 : prog -> env_loc -> object_loc -> out -> ext_expr
+  | spec_binding_inst_function_decls :  env_loc -> list funcdecl -> strictness_flag -> bool -> ext_expr
+  | spec_binding_inst_function_decls_1 : env_loc -> funcdecl -> list funcdecl -> strictness_flag -> bool -> out -> ext_expr
+  | spec_binding_inst_function_decls_2 : env_loc -> funcdecl -> list funcdecl -> strictness_flag -> object_loc -> bool -> out -> ext_expr
+  | spec_binding_inst_function_decls_3 : funcdecl -> list funcdecl -> strictness_flag -> object_loc -> bool -> specret full_descriptor -> ext_expr
+  | spec_binding_inst_function_decls_3a : funcdecl -> list funcdecl -> strictness_flag -> object_loc -> bool -> full_descriptor -> ext_expr
+  | spec_binding_inst_function_decls_4 : env_loc -> funcdecl -> list funcdecl -> strictness_flag -> object_loc -> bool -> out -> ext_expr
+  | spec_binding_inst_function_decls_5 : env_loc -> funcdecl -> list funcdecl -> strictness_flag -> object_loc -> bool -> ext_expr
+  | spec_binding_inst_function_decls_6 : env_loc -> list funcdecl -> strictness_flag -> bool -> out -> ext_expr
+  | spec_binding_inst_arg_obj :   object_loc -> list string -> list value -> env_loc -> strictness_flag -> ext_expr
+  | spec_binding_inst_arg_obj_1 : env_loc -> strictness_flag -> out -> ext_expr
+  | spec_binding_inst_arg_obj_2 : env_loc -> object_loc -> out -> ext_expr
   | spec_binding_inst_var_decls : env_loc -> list string -> bool -> strictness_flag -> ext_expr
   | spec_binding_inst_var_decls_1 : env_loc -> string -> list string -> bool -> strictness_flag -> out -> ext_expr
   | spec_binding_inst_var_decls_2 : env_loc -> list string -> bool -> strictness_flag -> out -> ext_expr
@@ -1148,17 +1148,17 @@ Definition out_of_ext_expr (e : ext_expr) : option out :=
   | spec_binding_inst_formal_params_2 _ _ _ _ _ _ o => Some o
   | spec_binding_inst_formal_params_3 _ _ _ _ _ _ => None
   | spec_binding_inst_formal_params_4 _ _ _ _ o => Some o
-  | spec_binding_inst_function_decls _ _ _ _ _ => None
-  | spec_binding_inst_function_decls_1 _ _ _ _ _ _ o => Some o
-  | spec_binding_inst_function_decls_2 _ _ _ _ _ _ _ o => Some o
-  | spec_binding_inst_function_decls_3 _ _ _ _ _ _ y => out_of_specret y
-  | spec_binding_inst_function_decls_3a _ _ _ _ _ _ _ => None
-  | spec_binding_inst_function_decls_4 _ _ _ _ _ _ _ o => Some o
-  | spec_binding_inst_function_decls_5 _ _ _ _ _ _ _ => None
-  | spec_binding_inst_function_decls_6 _ _ _ _ _ o => Some o
+  | spec_binding_inst_function_decls _ _ _ _ => None
+  | spec_binding_inst_function_decls_1 _ _ _ _ _ o => Some o
+  | spec_binding_inst_function_decls_2 _ _ _ _ _ _ o => Some o
+  | spec_binding_inst_function_decls_3 _ _ _ _ _ y => out_of_specret y
+  | spec_binding_inst_function_decls_3a _ _ _ _ _ _ => None
+  | spec_binding_inst_function_decls_4 _ _ _ _ _ _ o => Some o
+  | spec_binding_inst_function_decls_5 _ _ _ _ _ _ => None
+  | spec_binding_inst_function_decls_6 _ _ _ _ o => Some o
   | spec_binding_inst_arg_obj   object_loc _ _ _ _ => None
-  | spec_binding_inst_arg_obj_1 _ _ _ o => Some o
-  | spec_binding_inst_arg_obj_2 _ _ _ o => Some o
+  | spec_binding_inst_arg_obj_1 _ _ o => Some o
+  | spec_binding_inst_arg_obj_2 _ _ o => Some o
   | spec_binding_inst_var_decls _ _ _ _ => None
   | spec_binding_inst_var_decls_1 _ _ _ _ _ o => Some o
   | spec_binding_inst_var_decls_2 _ _ _ _ o => Some o