diff --git a/proto/region/vmxon.c b/proto/region/vmxon.c
new file mode 100644
index 0000000000000000000000000000000000000000..d4cd85f53d28bea45ef9bc207210527e9a7ba6ad
--- /dev/null
+++ b/proto/region/vmxon.c
@@ -0,0 +1,21 @@
+#include "../debug/debug.h"
+#include "../msr/msr.h"
+#include "vxmon.h"
+#include <asm/page.h>
+#include <linux/errno.h>
+#include <linux/printk.h>
+#include <linux/slab.h>
+
+struct vmxon_t *alloc_vmxon(void) {
+    struct vmxon_t *vmxon = kzalloc(sizeof(struct vmxon_t), GFP_KERNEL);
+
+    if (!vmxon) {
+        DEBUG_FMT("VMXON region allocation has failed\n");
+        return NULL;
+    }
+
+    vmxon->header.vmcs_rev_id = VMCS_REVISION_ID;
+    vmxon->header.shadow_vmcs = 0;
+
+    return vmxon;
+}
diff --git a/proto/region/vmxon_reg.c b/proto/region/vmxon_reg.c
deleted file mode 100644
index e4ade30d1cca337b52042320773380305d7237ac..0000000000000000000000000000000000000000
--- a/proto/region/vmxon_reg.c
+++ /dev/null
@@ -1,69 +0,0 @@
-#include "../debug/debug.h"
-#include "../msr/msr.h"
-#include "vxmon_reg.h"
-#include <asm/page.h>
-#include <linux/errno.h>
-#include <linux/printk.h>
-#include <linux/slab.h>
-
-static int alloc_vmxon_internals(struct vmxon_region_t *reg) {
-    if (!reg) {
-        DEBUG_FMT("vmxon_reg_t isn't allocated\n");
-        return -EFAULT;
-    }
-
-    void *region = kzalloc(PAGE_SIZE, GFP_KERNEL);
-
-    if (!region) {
-        DEBUG_FMT("VMXON region allocation has failed\n");
-        return -EFAULT;
-    }
-
-    if (((unsigned long long)region & 0xfff) != 0) {
-        DEBUG_FMT("Region 0x%px isn't properly aligned\n", region);
-        return -EFAULT;
-    }
-
-    DEBUG_FMT(
-        "Reading IA32_VMX_BASIC MSR for allocation size (in bytes) = %llu \n",
-        REGION_SIZE);
-
-    reg->size = REGION_SIZE;
-    reg->va = region;
-    reg->pa = __pa(region);
-
-    return 0;
-}
-
-static int write_vmcs_rev_id_to_vmxon(struct vmxon_region_t *reg) {
-    if (!reg) {
-        DEBUG_FMT("vmxon_reg_t isn't allocated\n");
-        return -EFAULT;
-    }
-
-    DEBUG_FMT(
-        "Reading IA32_VMX_BASIC MSR for VMCS revision identifier = 0x%llx\n",
-        VMCS_REVISION_ID);
-
-    DEBUG_FMT("Writing VMCS Revision ID to VMXON region\n");
-
-    (*(unsigned long *)reg->va) = VMCS_REVISION_ID;
-    (*(unsigned long *)reg->va) &= ~(1UL << 31);
-
-    return 0;
-}
-
-int init_vmxon_reg(struct vmxon_region_t *reg) {
-    int ret;
-
-    if ((ret = alloc_vmxon_internals(reg)) != 0) {
-        return ret;
-    }
-
-    if ((ret = write_vmcs_rev_id_to_vmxon(reg)) != 0) {
-        kfree(reg->va);
-        return ret;
-    }
-
-    return 0;
-}
diff --git a/proto/region/vxmon.h b/proto/region/vxmon.h
new file mode 100644
index 0000000000000000000000000000000000000000..c75c5d440fb1a56ece367638a5a8cd72a269c1f0
--- /dev/null
+++ b/proto/region/vxmon.h
@@ -0,0 +1,11 @@
+#pragma once
+
+struct vmxon_t {
+    struct {
+        unsigned long vmcs_rev_id : 31;
+        unsigned long shadow_vmcs : 1;
+    } header;
+    char state[0x1000 - sizeof(unsigned long)];
+};
+
+struct vmxon_t *alloc_vmxon(void);
diff --git a/proto/region/vxmon_reg.h b/proto/region/vxmon_reg.h
deleted file mode 100644
index e080b028ea6c1584f929382b353e8e3d12e85e62..0000000000000000000000000000000000000000
--- a/proto/region/vxmon_reg.h
+++ /dev/null
@@ -1,9 +0,0 @@
-#pragma once
-
-struct vmxon_region_t {
-    unsigned long size;
-    void *va;
-    unsigned long long pa;
-};
-
-int init_vmxon_reg(struct vmxon_region_t *reg);