From b3159a7069504fe2fb2b781cd6f438decaf0937a Mon Sep 17 00:00:00 2001
From: Adam Chlipala <adamc@hcoop.net>
Date: Sun, 10 Dec 2006 20:09:28 +0000
Subject: [PATCH] Limit 'extern' to trusted code

---
 src/main.sml    |  5 ++++-
 src/tycheck.sig |  3 +++
 src/tycheck.sml | 18 ++++++++++++++++--
 3 files changed, 23 insertions(+), 3 deletions(-)

diff --git a/src/main.sml b/src/main.sml
index 5b9ee57..2aa3da7 100644
--- a/src/main.sml
+++ b/src/main.sml
@@ -58,7 +58,9 @@ fun basis () =
 	if !ErrorMsg.anyErrors then
 	    Env.empty
 	else
-	    foldl (fn (fname, G) => check' G fname) Env.empty files
+	    (Tycheck.allowExterns ();
+	     foldl (fn (fname, G) => check' G fname) Env.empty files
+	     before Tycheck.disallowExterns ())
     end
 
 fun check fname =
@@ -72,6 +74,7 @@ fun check fname =
 	    raise ErrorMsg.Error
 	else
 	    let
+		val _ = Tycheck.disallowExterns ()
 		val _ = ErrorMsg.reset ()
 		val prog = Parse.parse fname
 	    in
diff --git a/src/tycheck.sig b/src/tycheck.sig
index 22b44c7..19ec6d4 100644
--- a/src/tycheck.sig
+++ b/src/tycheck.sig
@@ -35,4 +35,7 @@ signature TYCHECK = sig
 
     val preface : string * Print.PD.pp_desc -> unit
 
+    val allowExterns : unit -> unit
+    val disallowExterns : unit -> unit
+
 end
diff --git a/src/tycheck.sml b/src/tycheck.sml
index 9467b64..007a0fe 100644
--- a/src/tycheck.sml
+++ b/src/tycheck.sml
@@ -24,6 +24,10 @@ open Ast Print Env
 
 structure SM = StringMap
 
+val externFlag = ref false
+fun allowExterns () = externFlag := true
+fun disallowExterns () = externFlag := false
+
 local
     val unifCount = ref 0
 in
@@ -703,8 +707,18 @@ fun checkUnit G (eAll as (_, loc)) =
 
 fun checkDecl G (d, _, loc) =
     case d of
-	DExternType name => bindType G name
-      | DExternVal (name, t) => bindVal G (name, checkTyp G t, NONE)
+	DExternType name =>
+	if !externFlag then
+	    bindType G name
+	else
+	    (ErrorMsg.error (SOME loc) "'extern type' not allowed in untrusted code";
+	     G)
+      | DExternVal (name, t) =>
+	if !externFlag then
+	    bindVal G (name, checkTyp G t, NONE)
+	else
+	    (ErrorMsg.error (SOME loc) "'extern val' not allowed in untrusted code";
+	     G)
       | DVal (name, to, e) =>
 	let
 	    val to =
-- 
2.20.1