diff --git a/Pal/src/host/FreeBSD/pal.map b/Pal/src/host/FreeBSD/pal.map
index b623ee8a..708a4ef8 100644
--- a/Pal/src/host/FreeBSD/pal.map
+++ b/Pal/src/host/FreeBSD/pal.map
@@ -40,7 +40,7 @@ PAL {
         DkMemoryAvailableQuota;
 
         # Debugging ABIs
-        pal_printf; DkDebugAttachBinary; DkDebugDetachBinary;
+        pal_printf; pal_vprintf; DkDebugAttachBinary; DkDebugDetachBinary;
 
         # Control block
         pal_control_addr; pal_sec;
diff --git a/Pal/src/host/Linux-SGX/pal.map b/Pal/src/host/Linux-SGX/pal.map
index c41e4722..4ff78c0b 100644
--- a/Pal/src/host/Linux-SGX/pal.map
+++ b/Pal/src/host/Linux-SGX/pal.map
@@ -44,7 +44,7 @@ PAL {
         DkCpuIdRetrieve; # retrieve CPUID
 
         # Debugging ABIs
-        pal_printf; pal_snprintf; DkDebugAttachBinary; DkDebugDetachBinary;
+        pal_printf; pal_vprintf; pal_snprintf; DkDebugAttachBinary; DkDebugDetachBinary;
 
         # Control block
         pal_control; pal_control_addr;
diff --git a/Pal/src/host/Linux-SGX/sgx_graphene.c b/Pal/src/host/Linux-SGX/sgx_graphene.c
index 10bbb309..2db24fde 100644
--- a/Pal/src/host/Linux-SGX/sgx_graphene.c
+++ b/Pal/src/host/Linux-SGX/sgx_graphene.c
@@ -45,8 +45,8 @@ fputch(void * f, int ch, struct printbuf * b)
     return 0;
 }
 
-static int
-vprintf(const char * fmt, va_list ap)
+int
+pal_vprintf(const char * fmt, va_list ap)
 {
     struct printbuf b;
 
@@ -65,7 +65,7 @@ pal_printf(const char * fmt, ...)
     int cnt;
 
     va_start(ap, fmt);
-    cnt = vprintf(fmt, ap);
+    cnt = pal_vprintf(fmt, ap);
     va_end(ap);
 
     return cnt;
diff --git a/Pal/src/host/Linux/pal.map b/Pal/src/host/Linux/pal.map
index 1ce4b9bf..55be4b2d 100644
--- a/Pal/src/host/Linux/pal.map
+++ b/Pal/src/host/Linux/pal.map
@@ -41,7 +41,7 @@ PAL {
         DkMemoryAvailableQuota;
 
         # Debugging ABIs
-        pal_printf; DkDebugAttachBinary; DkDebugDetachBinary;
+        pal_printf; pal_vprintf; DkDebugAttachBinary; DkDebugDetachBinary;
 
         # Control block
         pal_control_addr; pal_sec;
diff --git a/Pal/src/host/Skeleton/pal.map b/Pal/src/host/Skeleton/pal.map
index 75c8a64d..4d0e3fe0 100644
--- a/Pal/src/host/Skeleton/pal.map
+++ b/Pal/src/host/Skeleton/pal.map
@@ -40,7 +40,7 @@ PAL {
         DkMemoryAvailableQuota;
 
         # Debugging ABIs
-        pal_printf; DkDebugAttachBinary; DkDebugDetachBinary;
+        pal_printf; pal_vprintf; DkDebugAttachBinary; DkDebugDetachBinary;
 
         # Control block
         pal_control_addr; pal_sec;
diff --git a/Pal/src/pal_debug.h b/Pal/src/pal_debug.h
index e5b336e7..8723b906 100644
--- a/Pal/src/pal_debug.h
+++ b/Pal/src/pal_debug.h
@@ -25,8 +25,10 @@
 
 #include "pal.h"
 #include <assert.h>
+#include <stdarg.h>
 
 int pal_printf (const char *fmt, ...) __attribute__((format(printf, 1, 2)));
+int pal_vprintf (const char *fmt, va_list ap) __attribute__((format(printf, 1, 0)));
 
 void DkDebugAttachBinary (PAL_STR uri, PAL_PTR start_addr);
 void DkDebugDetachBinary (PAL_PTR start_addr);
diff --git a/Pal/src/printf.c b/Pal/src/printf.c
index 864c6dad..3f4c0a5e 100644
--- a/Pal/src/printf.c
+++ b/Pal/src/printf.c
@@ -59,6 +59,7 @@ vprintf(const char * fmt, va_list ap)
 
     return b.cnt;
 }
+EXTERN_ALIAS(vprintf);
 
 int
 printf(const char * fmt, ...)