diff -r 3bb0b8cbb29c tboot/common/policy.c
--- a/tboot/common/policy.c	Thu Mar 26 14:34:18 2009 -0700
+++ b/tboot/common/policy.c	Wed Apr 15 10:18:13 2009 -0400
@@ -59,6 +59,7 @@
 
 extern void shutdown(void);
 extern void s3_launch(void);
+extern void unmeasured_launch(void);
 
 /* MLE/kernel shared data page (in boot.S) */
 extern tboot_shared_t _tboot_shared;
@@ -360,7 +361,7 @@
             if ( s3_flag )
                 s3_launch();
             else
-                launch_kernel(false);
+                unmeasured_launch();
             break; /* if launch xen fails, do halt at the end */
         case TB_POLACT_HALT:
             break; /* do halt at the end */
diff -r 3bb0b8cbb29c tboot/common/tboot.c
--- a/tboot/common/tboot.c	Thu Mar 26 14:34:18 2009 -0700
+++ b/tboot/common/tboot.c	Wed Apr 15 10:18:13 2009 -0400
@@ -513,6 +513,24 @@
     shutdown_system(_tboot_shared.shutdown_type);
 }
 
+void unmeasured_launch(void)
+{
+    void *base = NULL;
+
+    printk("unmeasured_launch() called\n");
+
+    /* unload all txt modules before an unmeasured launch - remove them */
+    /* so that VMM/kernel doesn't see extra files */
+    if ( txt_find_sinit_module(g_mbi, &base, NULL) )
+        if ( remove_module(g_mbi, base) == NULL )
+            printk("failed to remove SINIT module from module list\n");
+    if ( txt_find_lcp_module(g_mbi, &base, NULL) )
+        if ( remove_module(g_mbi, base) == NULL )
+            printk("failed to remove LCP module from module list\n");
+
+    launch_kernel(false);
+}
+
 void handle_exception(void)
 {
     printk("received exception; shutting down...\n");
diff -r 3bb0b8cbb29c tboot/include/txt/txt.h
--- a/tboot/include/txt/txt.h	Thu Mar 26 14:34:18 2009 -0700
+++ b/tboot/include/txt/txt.h	Wed Apr 15 10:18:13 2009 -0400
@@ -50,6 +50,10 @@
 extern bool txt_s3_launch_environment(void);
 extern void txt_shutdown(void);
 extern bool txt_is_powercycle_required(void);
+extern bool txt_find_sinit_module(multiboot_info_t *mbi, void **base,
+                                  uint32_t *size);
+extern bool txt_find_lcp_module(multiboot_info_t *mbi, void **base,
+                                  uint32_t *size);
 
 #endif      /* __TXT_TXT_H__ */
 
diff -r 3bb0b8cbb29c tboot/txt/txt.c
--- a/tboot/txt/txt.c	Thu Mar 26 14:34:18 2009 -0700
+++ b/tboot/txt/txt.c	Wed Apr 15 10:18:13 2009 -0400
@@ -190,7 +190,8 @@
 }
 
 /* size can be NULL */
-static bool find_sinit(multiboot_info_t *mbi, void **base, uint32_t *size)
+bool txt_find_sinit_module(multiboot_info_t *mbi, void **base,
+                           uint32_t *size)
 {
     module_t *mods;
     uint32_t size2 = 0;
@@ -198,7 +199,7 @@
     int i;
 
     if ( base == NULL ) {
-        printk("find_sinit() base is NULL\n");
+        printk("txt_find_sinit_module() base is NULL\n");
         return false;
     }
     *base = NULL;
@@ -231,14 +232,14 @@
     return true;
 }
 
-static bool find_lcp_manifest(multiboot_info_t *mbi, void **base,
-                              uint32_t *size)
+bool txt_find_lcp_module(multiboot_info_t *mbi, void **base,
+                         uint32_t *size)
 {
     size_t size2 = 0;
     void *base2 = NULL;
 
     if ( base == NULL ) {
-        printk("find_lcp_manifest() base is NULL\n");
+        printk("txt_find_lcp_module() base is NULL\n");
         return false;
     }
     *base = NULL;
@@ -315,7 +316,7 @@
     /* LCP manifest */
     void *lcp_base = NULL;
     uint32_t lcp_size = 0;
-    find_lcp_manifest(mbi, &lcp_base, &lcp_size);
+    txt_find_lcp_module(mbi, &lcp_base, &lcp_size);
     os_sinit_data->lcp_po_base = (unsigned long)lcp_base;
     os_sinit_data->lcp_po_size = lcp_size;
     /* if we found a manifest, remove it from module list so that */
@@ -477,7 +478,7 @@
     /*
      * find SINIT AC module in modules list (it should be one of last three)
      */
-    if ( find_sinit(mbi, (void **)&sinit, NULL) ) {
+    if ( txt_find_sinit_module(mbi, (void **)&sinit, NULL) ) {
         /* check if it matches chipset */
         if ( !does_acmod_match_chipset(sinit) ) {
             printk("SINIT does not match chipset\n");