diff --git a/src/arch/x86/kernel/boot_sys.c b/src/arch/x86/kernel/boot_sys.c
index 2eb8ecfb6e15d69926f450fcfffe17c7e49bb46b..3ff69c8db0b8c31c58a46472484067e56e07eb9e 100644
--- a/src/arch/x86/kernel/boot_sys.c
+++ b/src/arch/x86/kernel/boot_sys.c
@@ -71,7 +71,7 @@ boot_state_t boot_state;
 
 /* There are a lot of assumptions on this being page aligned and
  * precisely 4K in size. DO NOT MODIFY */
-ALIGN(BIT(PAGE_BITS))
+ALIGN(BIT(PAGE_BITS)) VISIBLE
 char kernel_stack_alloc[4096];
 
 /* global variables (not covered by abstract specification) */