diff --git a/core/embed/kernel/main.c b/core/embed/kernel/main.c
index db314137da..f6194a705a 100644
--- a/core/embed/kernel/main.c
+++ b/core/embed/kernel/main.c
@@ -183,10 +183,21 @@ static void coreapp_init(applet_t *applet) {
       (applet_header_t *)COREAPP_CODE_ALIGN(KERNEL_START + KERNEL_SIZE);
 
   applet_layout_t coreapp_layout = {
-      .data1_start = (uint32_t)&_coreapp_clear_ram_0_start,
-      .data1_size = (uint32_t)&_coreapp_clear_ram_0_size,
-      .data2_start = (uint32_t)&_coreapp_clear_ram_1_start,
-      .data2_size = (uint32_t)&_coreapp_clear_ram_1_size,
+      .data1.start = (uint32_t)&_coreapp_clear_ram_0_start,
+      .data1.size = (uint32_t)&_coreapp_clear_ram_0_size,
+      .data2.start = (uint32_t)&_coreapp_clear_ram_1_start,
+      .data2.size = (uint32_t)&_coreapp_clear_ram_1_size,
+#ifdef FIRMWARE_P1_START
+      .code1.start = FIRMWARE_P1_START + KERNEL_SIZE,
+      .code1.size = FIRMWARE_P1_MAXSIZE - KERNEL_SIZE,
+      .code2.start = FIRMWARE_P2_START,
+      .code2.size = FIRMWARE_P2_MAXSIZE,
+#else
+      .code1.start = FIRMWARE_START + KERNEL_SIZE,
+      .code1.size = FIRMWARE_MAXSIZE - KERNEL_SIZE,
+      .code2.start = 0,
+      .code2.size = 0,
+#endif
   };
 
   applet_init(applet, coreapp_header, &coreapp_layout);
diff --git a/core/embed/trezorhal/applet.h b/core/embed/trezorhal/applet.h
index 5309e7b5d8..afdfb25810 100644
--- a/core/embed/trezorhal/applet.h
+++ b/core/embed/trezorhal/applet.h
@@ -30,23 +30,29 @@
 // Applet entry point
 typedef void (*applet_startup_t)(const char* args, uint32_t random);
 
+typedef struct {
+  uint32_t start;
+  uint32_t size;
+} memory_area_t;
+
 // Applet header found at the beginning of the applet binary
 typedef struct {
   // Stack area
-  uint32_t stack_start;
-  uint32_t stack_size;
+  memory_area_t stack;
   // Applet entry point
   applet_startup_t startup;
 } applet_header_t;
 
 // Applet memory layout
 typedef struct {
-  // Data area 1
-  uint32_t data1_start;
-  uint32_t data1_size;
-  // Data area 2
-  uint32_t data2_start;
-  uint32_t data2_size;
+  // Read/write data area #1
+  memory_area_t data1;
+  // Read/write data area #2
+  memory_area_t data2;
+  // Read-only code area #1
+  memory_area_t code1;
+  // Read-only code area #2
+  memory_area_t code2;
 
 } applet_layout_t;
 
@@ -76,6 +82,11 @@ void applet_init(applet_t* applet, applet_header_t* header,
 bool applet_reset(applet_t* applet, uint32_t cmd, const void* arg,
                   size_t arg_size);
 
+// Returns the currently active applet.
+//
+// Returns `NULL` if no applet is currently active.
+applet_t* applet_active(void);
+
 #endif  // SYSCALL_DISPATCH
 
 #endif  // TREZORHAL_APPLET_H
diff --git a/core/embed/trezorhal/stm32f4/applet.c b/core/embed/trezorhal/stm32f4/applet.c
index a36e2f9cf3..67a3e0fcd6 100644
--- a/core/embed/trezorhal/stm32f4/applet.c
+++ b/core/embed/trezorhal/stm32f4/applet.c
@@ -35,11 +35,11 @@ void applet_init(applet_t* applet, applet_header_t* header,
 }
 
 static void applet_clear_memory(applet_t* applet) {
-  if (applet->layout.data1_size > 0) {
-    memset((void*)applet->layout.data1_start, 0, applet->layout.data1_size);
+  if (applet->layout.data1.size > 0) {
+    memset((void*)applet->layout.data1.start, 0, applet->layout.data1.size);
   }
-  if (applet->layout.data2_size > 0) {
-    memset((void*)applet->layout.data2_start, 0, applet->layout.data2_size);
+  if (applet->layout.data2.size > 0) {
+    memset((void*)applet->layout.data2.start, 0, applet->layout.data2.size);
   }
 }
 
@@ -49,8 +49,8 @@ bool applet_reset(applet_t* applet, uint32_t cmd, const void* arg,
   applet_clear_memory(applet);
 
   // Reset the applet task (stack pointer, etc.)
-  systask_init(&applet->task, applet->header->stack_start,
-               applet->header->stack_size);
+  systask_init(&applet->task, applet->header->stack.start,
+               applet->header->stack.size, applet);
 
   // Copy the arguments onto the applet stack
   void* arg_copy = NULL;
@@ -70,4 +70,14 @@ bool applet_reset(applet_t* applet, uint32_t cmd, const void* arg,
                            arg3);
 }
 
+applet_t* applet_active(void) {
+  systask_t* task = systask_active();
+
+  if (task == NULL) {
+    return NULL;
+  }
+
+  return (applet_t*)task->applet;
+}
+
 #endif  // SYSCALL_DISPATCH
diff --git a/core/embed/trezorhal/stm32f4/syscall_dispatch.c b/core/embed/trezorhal/stm32f4/syscall_dispatch.c
index 2844a2bc40..9698f345d3 100644
--- a/core/embed/trezorhal/stm32f4/syscall_dispatch.c
+++ b/core/embed/trezorhal/stm32f4/syscall_dispatch.c
@@ -46,6 +46,8 @@
 #include "usb_vcp.h"
 #include "usb_webusb.h"
 
+#include "syscall_verifiers.h"
+
 #ifdef SYSCALL_DISPATCH
 
 static PIN_UI_WAIT_CALLBACK storage_init_callback = NULL;
@@ -68,31 +70,28 @@ __attribute((no_stack_protector)) void syscall_handler(uint32_t *args,
                                                        uint32_t syscall) {
   switch (syscall) {
     case SYSCALL_SYSTEM_EXIT: {
-      systask_t *task = systask_active();
       int exit_code = (int)args[0];
-      systask_exit(task, exit_code);
+      system_exit__verified(exit_code);
     } break;
 
     case SYSCALL_SYSTEM_EXIT_ERROR: {
-      systask_t *task = systask_active();
       const char *title = (const char *)args[0];
       size_t title_len = (size_t)args[1];
       const char *message = (const char *)args[2];
       size_t message_len = (size_t)args[3];
       const char *footer = (const char *)args[4];
       size_t footer_len = (size_t)args[5];
-      systask_exit_error(task, title, title_len, message, message_len, footer,
-                         footer_len);
+      system_exit_error__verified(title, title_len, message, message_len,
+                                  footer, footer_len);
     } break;
 
     case SYSCALL_SYSTEM_EXIT_FATAL: {
-      systask_t *task = systask_active();
       const char *message = (const char *)args[0];
       size_t message_len = (size_t)args[1];
       const char *file = (const char *)args[2];
       size_t file_len = (size_t)args[3];
       int line = (int)args[4];
-      systask_exit_fatal(task, message, message_len, file, file_len, line);
+      system_exit_fatal__verified(message, message_len, file, file_len, line);
     } break;
 
     case SYSCALL_SYSTICK_CYCLES: {
@@ -123,7 +122,7 @@ __attribute((no_stack_protector)) void syscall_handler(uint32_t *args,
     } break;
 
     case SYSCALL_REBOOT_DEVICE: {
-      reboot();
+      reboot_device();
     } break;
 
     case SYSCALL_REBOOT_TO_BOOTLOADER: {
@@ -132,7 +131,7 @@ __attribute((no_stack_protector)) void syscall_handler(uint32_t *args,
 
     case SYSCALL_REBOOT_AND_UPGRADE: {
       const uint8_t *hash = (const uint8_t *)args[0];
-      reboot_and_upgrade(hash);
+      reboot_and_upgrade__verified(hash);
     } break;
 
     case SYSCALL_DISPLAY_SET_BACKLIGHT: {
@@ -156,7 +155,7 @@ __attribute((no_stack_protector)) void syscall_handler(uint32_t *args,
 #if XFRAMEBUFFER
     case SYSCALL_DISPLAY_GET_FB_INFO: {
       display_fb_info_t *fb = (display_fb_info_t *)args[0];
-      args[0] = (uint32_t)display_get_frame_buffer(fb);
+      args[0] = (uint32_t)display_get_frame_buffer__verified(fb);
     } break;
 #else
     case SYSCALL_DISPLAY_WAIT_FOR_SYNC: {
@@ -166,13 +165,13 @@ __attribute((no_stack_protector)) void syscall_handler(uint32_t *args,
 
     case SYSCALL_DISPLAY_FILL: {
       const gfx_bitblt_t *bb = (const gfx_bitblt_t *)args[0];
-      display_fill(bb);
+      display_fill__verified(bb);
     } break;
 
 #ifdef USE_RGB_COLORS
     case SYSCALL_DISPLAY_COPY_RGB565: {
       const gfx_bitblt_t *bb = (const gfx_bitblt_t *)args[0];
-      display_copy_rgb565(bb);
+      display_copy_rgb565__verified(bb);
     } break;
 #endif
 
@@ -220,14 +219,14 @@ __attribute((no_stack_protector)) void syscall_handler(uint32_t *args,
       uint8_t iface_num = (uint8_t)args[0];
       uint8_t *buf = (uint8_t *)args[1];
       uint32_t len = args[2];
-      args[0] = usb_hid_read(iface_num, buf, len);
+      args[0] = usb_hid_read__verified(iface_num, buf, len);
     } break;
 
     case SYSCALL_USB_HID_WRITE: {
       uint8_t iface_num = (uint8_t)args[0];
       const uint8_t *buf = (const uint8_t *)args[1];
       uint32_t len = args[2];
-      args[0] = usb_hid_write(iface_num, buf, len);
+      args[0] = usb_hid_write__verified(iface_num, buf, len);
     } break;
 
     case SYSCALL_USB_HID_READ_SELECT: {
@@ -240,7 +239,7 @@ __attribute((no_stack_protector)) void syscall_handler(uint32_t *args,
       uint8_t *buf = (uint8_t *)args[1];
       uint32_t len = args[2];
       int timeout = (int)args[3];
-      args[0] = usb_hid_read_blocking(iface_num, buf, len, timeout);
+      args[0] = usb_hid_read_blocking__verified(iface_num, buf, len, timeout);
     } break;
 
     case SYSCALL_USB_HID_WRITE_BLOCKING: {
@@ -248,7 +247,7 @@ __attribute((no_stack_protector)) void syscall_handler(uint32_t *args,
       const uint8_t *buf = (const uint8_t *)args[1];
       uint32_t len = args[2];
       int timeout = (int)args[3];
-      args[0] = usb_hid_write_blocking(iface_num, buf, len, timeout);
+      args[0] = usb_hid_write_blocking__verified(iface_num, buf, len, timeout);
     } break;
 
     case SYSCALL_USB_VCP_ADD: {
@@ -270,14 +269,14 @@ __attribute((no_stack_protector)) void syscall_handler(uint32_t *args,
       uint8_t iface_num = (uint8_t)args[0];
       uint8_t *buf = (uint8_t *)args[1];
       uint32_t len = args[2];
-      args[0] = usb_vcp_read(iface_num, buf, len);
+      args[0] = usb_vcp_read__verified(iface_num, buf, len);
     } break;
 
     case SYSCALL_USB_VCP_WRITE: {
       uint8_t iface_num = (uint8_t)args[0];
       const uint8_t *buf = (const uint8_t *)args[1];
       uint32_t len = args[2];
-      args[0] = usb_vcp_write(iface_num, buf, len);
+      args[0] = usb_vcp_write__verified(iface_num, buf, len);
     } break;
 
     case SYSCALL_USB_VCP_READ_BLOCKING: {
@@ -285,7 +284,7 @@ __attribute((no_stack_protector)) void syscall_handler(uint32_t *args,
       uint8_t *buf = (uint8_t *)args[1];
       uint32_t len = args[2];
       int timeout = (int)args[3];
-      args[0] = usb_vcp_read_blocking(iface_num, buf, len, timeout);
+      args[0] = usb_vcp_read_blocking__verified(iface_num, buf, len, timeout);
     } break;
 
     case SYSCALL_USB_VCP_WRITE_BLOCKING: {
@@ -293,7 +292,7 @@ __attribute((no_stack_protector)) void syscall_handler(uint32_t *args,
       const uint8_t *buf = (const uint8_t *)args[1];
       uint32_t len = args[2];
       int timeout = (int)args[3];
-      args[0] = usb_vcp_write_blocking(iface_num, buf, len, timeout);
+      args[0] = usb_vcp_write_blocking__verified(iface_num, buf, len, timeout);
     } break;
 
     case SYSCALL_USB_WEBUSB_ADD: {
@@ -315,14 +314,14 @@ __attribute((no_stack_protector)) void syscall_handler(uint32_t *args,
       uint8_t iface_num = (uint8_t)args[0];
       uint8_t *buf = (uint8_t *)args[1];
       uint32_t len = args[2];
-      args[0] = usb_webusb_read(iface_num, buf, len);
+      args[0] = usb_webusb_read__verified(iface_num, buf, len);
     } break;
 
     case SYSCALL_USB_WEBUSB_WRITE: {
       uint8_t iface_num = (uint8_t)args[0];
       const uint8_t *buf = (const uint8_t *)args[1];
       uint32_t len = args[2];
-      args[0] = usb_webusb_write(iface_num, buf, len);
+      args[0] = usb_webusb_write__verified(iface_num, buf, len);
     } break;
 
     case SYSCALL_USB_WEBUSB_READ_SELECT: {
@@ -335,7 +334,8 @@ __attribute((no_stack_protector)) void syscall_handler(uint32_t *args,
       uint8_t *buf = (uint8_t *)args[1];
       uint32_t len = args[2];
       int timeout = (int)args[3];
-      args[0] = usb_webusb_read_blocking(iface_num, buf, len, timeout);
+      args[0] =
+          usb_webusb_read_blocking__verified(iface_num, buf, len, timeout);
     } break;
 
     case SYSCALL_USB_WEBUSB_WRITE_BLOCKING: {
@@ -343,7 +343,8 @@ __attribute((no_stack_protector)) void syscall_handler(uint32_t *args,
       const uint8_t *buf = (const uint8_t *)args[1];
       uint32_t len = args[2];
       int timeout = (int)args[3];
-      args[0] = usb_webusb_write_blocking(iface_num, buf, len, timeout);
+      args[0] =
+          usb_webusb_write_blocking__verified(iface_num, buf, len, timeout);
     } break;
 
 #ifdef USE_SD_CARD
@@ -367,14 +368,14 @@ __attribute((no_stack_protector)) void syscall_handler(uint32_t *args,
       uint32_t *dest = (uint32_t *)args[0];
       uint32_t block_num = args[1];
       uint32_t num_blocks = args[2];
-      args[0] = sdcard_read_blocks(dest, block_num, num_blocks);
+      args[0] = sdcard_read_blocks__verified(dest, block_num, num_blocks);
     } break;
 
     case SYSCALL_SDCARD_WRITE_BLOCKS: {
       const uint32_t *src = (const uint32_t *)args[0];
       uint32_t block_num = args[1];
       uint32_t num_blocks = args[2];
-      args[0] = sdcard_write_blocks(src, block_num, num_blocks);
+      args[0] = sdcard_write_blocks__verified(src, block_num, num_blocks);
     } break;
 #endif
 
@@ -445,7 +446,7 @@ __attribute((no_stack_protector)) void syscall_handler(uint32_t *args,
     case SYSCALL_OPTIGA_CERT_SIZE: {
       uint8_t index = args[0];
       size_t *cert_size = (size_t *)args[1];
-      args[0] = optiga_cert_size(index, cert_size);
+      args[0] = optiga_cert_size__verified(index, cert_size);
     } break;
 
     case SYSCALL_OPTIGA_READ_CERT: {
@@ -453,18 +454,19 @@ __attribute((no_stack_protector)) void syscall_handler(uint32_t *args,
       uint8_t *cert = (uint8_t *)args[1];
       size_t max_cert_size = args[2];
       size_t *cert_size = (size_t *)args[3];
-      args[0] = optiga_read_cert(index, cert, max_cert_size, cert_size);
+      args[0] =
+          optiga_read_cert__verified(index, cert, max_cert_size, cert_size);
     } break;
 
     case SYSCALL_OPTIGA_READ_SEC: {
       uint8_t *sec = (uint8_t *)args[0];
-      args[0] = optiga_read_sec(sec);
+      args[0] = optiga_read_sec__verified(sec);
     } break;
 
     case SYSCALL_OPTIGA_RANDOM_BUFFER: {
       uint8_t *dest = (uint8_t *)args[0];
       size_t size = args[1];
-      args[0] = optiga_random_buffer(dest, size);
+      args[0] = optiga_random_buffer__verified(dest, size);
     } break;
 
 #if PYOPT == 0
@@ -479,7 +481,7 @@ __attribute((no_stack_protector)) void syscall_handler(uint32_t *args,
       const uint8_t *salt = (const uint8_t *)args[1];
       uint16_t salt_len = args[2];
       mpu_reconfig(MPU_MODE_STORAGE);
-      storage_init(storage_init_callback_wrapper, salt, salt_len);
+      storage_init__verified(storage_init_callback_wrapper, salt, salt_len);
     } break;
 
     case SYSCALL_STORAGE_WIPE: {
@@ -502,7 +504,7 @@ __attribute((no_stack_protector)) void syscall_handler(uint32_t *args,
       size_t pin_len = args[1];
       const uint8_t *ext_salt = (const uint8_t *)args[2];
       mpu_reconfig(MPU_MODE_STORAGE);
-      args[0] = storage_unlock(pin, pin_len, ext_salt);
+      args[0] = storage_unlock__verified(pin, pin_len, ext_salt);
     } break;
 
     case SYSCALL_STORAGE_HAS_PIN: {
@@ -528,15 +530,15 @@ __attribute((no_stack_protector)) void syscall_handler(uint32_t *args,
       const uint8_t *old_ext_salt = (const uint8_t *)args[4];
       const uint8_t *new_ext_salt = (const uint8_t *)args[5];
       mpu_reconfig(MPU_MODE_STORAGE);
-      args[0] = storage_change_pin(oldpin, oldpin_len, newpin, newpin_len,
-                                   old_ext_salt, new_ext_salt);
+      args[0] = storage_change_pin__verified(
+          oldpin, oldpin_len, newpin, newpin_len, old_ext_salt, new_ext_salt);
     } break;
 
     case SYSCALL_STORAGE_ENSURE_NOT_WIPE_CODE: {
       const uint8_t *pin = (const uint8_t *)args[0];
       size_t pin_len = args[1];
       mpu_reconfig(MPU_MODE_STORAGE);
-      storage_ensure_not_wipe_code(pin, pin_len);
+      storage_ensure_not_wipe_code__verified(pin, pin_len);
     } break;
 
     case SYSCALL_STORAGE_HAS_WIPE_CODE: {
@@ -551,8 +553,8 @@ __attribute((no_stack_protector)) void syscall_handler(uint32_t *args,
       const uint8_t *wipe_code = (const uint8_t *)args[3];
       size_t wipe_code_len = args[4];
       mpu_reconfig(MPU_MODE_STORAGE);
-      args[0] = storage_change_wipe_code(pin, pin_len, ext_salt, wipe_code,
-                                         wipe_code_len);
+      args[0] = storage_change_wipe_code__verified(pin, pin_len, ext_salt,
+                                                   wipe_code, wipe_code_len);
     } break;
 
     case SYSCALL_STORAGE_HAS: {
@@ -567,7 +569,7 @@ __attribute((no_stack_protector)) void syscall_handler(uint32_t *args,
       uint16_t max_len = (uint16_t)args[2];
       uint16_t *len = (uint16_t *)args[3];
       mpu_reconfig(MPU_MODE_STORAGE);
-      args[0] = storage_get(key, val, max_len, len);
+      args[0] = storage_get__verified(key, val, max_len, len);
     } break;
 
     case SYSCALL_STORAGE_SET: {
@@ -575,7 +577,7 @@ __attribute((no_stack_protector)) void syscall_handler(uint32_t *args,
       const void *val = (const void *)args[1];
       uint16_t len = (uint16_t)args[2];
       mpu_reconfig(MPU_MODE_STORAGE);
-      args[0] = storage_set(key, val, len);
+      args[0] = storage_set__verified(key, val, len);
     } break;
 
     case SYSCALL_STORAGE_DELETE: {
@@ -595,12 +597,12 @@ __attribute((no_stack_protector)) void syscall_handler(uint32_t *args,
       uint16_t key = (uint16_t)args[0];
       uint32_t *count = (uint32_t *)args[1];
       mpu_reconfig(MPU_MODE_STORAGE);
-      args[0] = storage_next_counter(key, count);
+      args[0] = storage_next_counter__verified(key, count);
     } break;
 
     case SYSCALL_ENTROPY_GET: {
       uint8_t *buf = (uint8_t *)args[0];
-      entropy_get(buf);
+      entropy_get__verified(buf);
     } break;
 
     case SYSCALL_TRANSLATIONS_WRITE: {
@@ -631,7 +633,7 @@ __attribute((no_stack_protector)) void syscall_handler(uint32_t *args,
     case SYSCALL_FIRMWARE_GET_VENDOR: {
       char *buff = (char *)args[0];
       size_t buff_size = args[1];
-      args[0] = firmware_get_vendor(buff, buff_size);
+      args[0] = firmware_get_vendor__verified(buff, buff_size);
     } break;
 
     case SYSCALL_FIRMWARE_CALC_HASH: {
@@ -642,9 +644,9 @@ __attribute((no_stack_protector)) void syscall_handler(uint32_t *args,
       firmware_hash_callback = (firmware_hash_callback_t)args[4];
       void *callback_context = (void *)args[5];
 
-      args[0] =
-          firmware_calc_hash(challenge, challenge_len, hash, hash_len,
-                             firmware_hash_callback_wrapper, callback_context);
+      args[0] = firmware_calc_hash__verified(
+          challenge, challenge_len, hash, hash_len,
+          firmware_hash_callback_wrapper, callback_context);
     } break;
 
     default:
diff --git a/core/embed/trezorhal/stm32f4/syscall_probe.c b/core/embed/trezorhal/stm32f4/syscall_probe.c
new file mode 100644
index 0000000000..525b396a1d
--- /dev/null
+++ b/core/embed/trezorhal/stm32f4/syscall_probe.c
@@ -0,0 +1,103 @@
+/*
+ * This file is part of the Trezor project, https://trezor.io/
+ *
+ * Copyright (c) SatoshiLabs
+ *
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <http://www.gnu.org/licenses/>.
+ */
+
+#include "syscall_probe.h"
+#include "applet.h"
+#include "model.h"
+
+#ifdef SYSCALL_DISPATCH
+
+static inline bool inside_area(const void *addr, size_t len,
+                               const memory_area_t *area) {
+  return ((uintptr_t)addr >= area->start) &&
+         ((uintptr_t)addr + len <= area->start + area->size);
+}
+
+bool probe_read_access(const void *addr, size_t len) {
+  applet_t *applet = applet_active();
+
+  if (applet == NULL) {
+    return false;
+  }
+
+  if (addr == NULL) {
+    return true;
+  }
+
+  // Address overflow check
+  if ((uintptr_t)addr + len < (uintptr_t)addr) {
+    return false;
+  }
+
+  if (inside_area(addr, len, &applet->layout.data1)) {
+    return true;
+  }
+
+  if (inside_area(addr, len, &applet->layout.data2)) {
+    return true;
+  }
+
+  if (inside_area(addr, len, &applet->layout.code1)) {
+    return true;
+  }
+
+  if (inside_area(addr, len, &applet->layout.code2)) {
+    return true;
+  }
+
+  static const memory_area_t assets = {
+      .start = ASSETS_START,
+      .size = ASSETS_MAXSIZE,
+  };
+
+  if (inside_area(addr, len, &assets)) {
+    return true;
+  }
+
+  return false;
+}
+
+bool probe_write_access(void *addr, size_t len) {
+  applet_t *applet = applet_active();
+
+  if (applet == NULL) {
+    return false;
+  }
+
+  if (addr == NULL) {
+    return true;
+  }
+
+  // Address overflow check
+  if ((uintptr_t)addr + len < (uintptr_t)addr) {
+    return false;
+  }
+
+  if (inside_area(addr, len, &applet->layout.data1)) {
+    return true;
+  }
+
+  if (inside_area(addr, len, &applet->layout.data2)) {
+    return true;
+  }
+
+  return false;
+}
+
+#endif  // SYSCALL_DISPATCH
diff --git a/core/embed/trezorhal/stm32f4/syscall_probe.h b/core/embed/trezorhal/stm32f4/syscall_probe.h
new file mode 100644
index 0000000000..b3353ef890
--- /dev/null
+++ b/core/embed/trezorhal/stm32f4/syscall_probe.h
@@ -0,0 +1,47 @@
+/*
+ * This file is part of the Trezor project, https://trezor.io/
+ *
+ * Copyright (c) SatoshiLabs
+ *
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <http://www.gnu.org/licenses/>.
+ */
+
+#ifndef TREZORHAL_SYSCALL_PROBE_H
+#define TREZORHAL_SYSCALL_PROBE_H
+
+#include <stdbool.h>
+#include <stddef.h>
+
+#include "system.h"
+
+#ifdef SYSCALL_DISPATCH
+
+// Checks if the current application task has read access to the
+// given memory range.
+bool probe_read_access(const void *addr, size_t len);
+
+// Checks if the current application task has write access to the
+// given memory range.
+bool probe_write_access(void *addr, size_t len);
+
+// Exits the current application task with an fatal error
+// with the message "Access violation".
+#define apptask_access_violation()                             \
+  do {                                                         \
+    system_exit_fatal("Access violation", __FILE__, __LINE__); \
+  } while (0)
+
+#endif  // SYSCALL_DISPATCH
+
+#endif  // TREZORHAL_SYSCALL_PROBE_H
diff --git a/core/embed/trezorhal/stm32f4/syscall_verifiers.c b/core/embed/trezorhal/stm32f4/syscall_verifiers.c
new file mode 100644
index 0000000000..2573a89cd3
--- /dev/null
+++ b/core/embed/trezorhal/stm32f4/syscall_verifiers.c
@@ -0,0 +1,660 @@
+/*
+ * This file is part of the Trezor project, https://trezor.io/
+ *
+ * Copyright (c) SatoshiLabs
+ *
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <http://www.gnu.org/licenses/>.
+ */
+
+#include <string.h>
+
+#include "common.h"
+#include "syscall_probe.h"
+#include "syscall_verifiers.h"
+#include "systask.h"
+
+#ifdef SYSCALL_DISPATCH
+
+// ---------------------------------------------------------------------
+
+void system_exit__verified(int exit_code) {
+  systask_t *task = systask_active();
+
+  systask_exit(task, exit_code);
+}
+
+void system_exit_error__verified(const char *title, size_t title_len,
+                                 const char *message, size_t message_len,
+                                 const char *footer, size_t footer_len) {
+  char title_copy[64] = {0};
+  char message_copy[64] = {0};
+  char footer_copy[64] = {0};
+
+  if (title != NULL) {
+    if (!probe_read_access(title, title_len)) {
+      goto access_violation;
+    }
+    title_len = MIN(title_len, sizeof(title_copy) - 1);
+    title = strncpy(title_copy, title, title_len);
+  } else {
+    title_len = 0;
+  }
+
+  if (message != NULL) {
+    if (!probe_read_access(message, message_len)) {
+      goto access_violation;
+    }
+    message_len = MIN(message_len, sizeof(message_copy) - 1);
+    message = strncpy(message_copy, message, message_len);
+  } else {
+    message_len = 0;
+  }
+
+  if (footer != NULL) {
+    if (!probe_read_access(footer, footer_len)) {
+      goto access_violation;
+    }
+    footer_len = MIN(footer_len, sizeof(footer_copy) - 1);
+    footer = strncpy(footer_copy, footer, footer_len);
+  } else {
+    footer_len = 0;
+  }
+
+  systask_t *task = systask_active();
+
+  systask_exit_error(task, title, title_len, message, message_len, footer,
+                     footer_len);
+
+  return;
+
+access_violation:
+  apptask_access_violation();
+}
+
+void system_exit_fatal__verified(const char *message, size_t message_len,
+                                 const char *file, size_t file_len, int line) {
+  char message_copy[64] = {0};
+  char file_copy[64] = {0};
+
+  if (message != NULL) {
+    if (!probe_read_access(message, message_len)) {
+      goto access_violation;
+    }
+    message_len = MIN(message_len, sizeof(message_copy) - 1);
+    message = strncpy(message_copy, message, message_len);
+  } else {
+    message_len = 0;
+  }
+
+  if (file != NULL) {
+    if (!probe_read_access(file, file_len)) {
+      goto access_violation;
+    }
+    file_len = MIN(file_len, sizeof(file_copy) - 1);
+    file = strncpy(file_copy, file, file_len);
+  } else {
+    file_len = 0;
+  }
+
+  systask_t *task = systask_active();
+
+  systask_exit_fatal(task, message, message_len, file, file_len, line);
+
+  return;
+
+access_violation:
+  apptask_access_violation();
+}
+
+// ---------------------------------------------------------------------
+
+void reboot_and_upgrade__verified(const uint8_t hash[32]) {
+  if (!probe_read_access(hash, 32)) {
+    goto access_violation;
+  }
+
+  reboot_and_upgrade(hash);
+
+access_violation:
+  apptask_access_violation();
+}
+
+// ---------------------------------------------------------------------
+
+#ifdef XFRAMEBUFFER
+
+bool display_get_frame_buffer__verified(display_fb_info_t *fb) {
+  if (!probe_write_access(fb, sizeof(*fb))) {
+    goto access_violation;
+  }
+
+  display_fb_info_t fb_copy = {0};
+
+  bool result = display_get_frame_buffer(&fb_copy);
+
+  *fb = fb_copy;
+
+  return result;
+
+access_violation:
+  apptask_access_violation();
+  return false;
+}
+
+#endif  // XFRAMEBUFFER
+
+void display_fill__verified(const gfx_bitblt_t *bb) {
+  if (!probe_read_access(bb, sizeof(*bb))) {
+    goto access_violation;
+  }
+
+  gfx_bitblt_t bb_copy = *bb;
+
+  display_fill(&bb_copy);
+
+  return;
+
+access_violation:
+  apptask_access_violation();
+}
+
+void display_copy_rgb565__verified(const gfx_bitblt_t *bb) {
+  if (!probe_read_access(bb, sizeof(*bb))) {
+    goto access_violation;
+  }
+
+  gfx_bitblt_t bb_copy = *bb;
+
+  uint8_t *src_ptr = (uint8_t *)bb_copy.src_row;
+  size_t src_len = bb_copy.src_stride * bb_copy.height;
+
+  if (!probe_read_access(src_ptr, src_len)) {
+    goto access_violation;
+  }
+
+  display_copy_rgb565(&bb_copy);
+
+  return;
+
+access_violation:
+  apptask_access_violation();
+}
+
+// ---------------------------------------------------------------------
+
+int usb_hid_read__verified(uint8_t iface_num, uint8_t *buf, uint32_t len) {
+  if (!probe_write_access(buf, len)) {
+    goto access_violation;
+  }
+
+  return usb_hid_read(iface_num, buf, len);
+
+access_violation:
+  apptask_access_violation();
+  return 0;
+}
+
+int usb_hid_write__verified(uint8_t iface_num, const uint8_t *buf,
+                            uint32_t len) {
+  if (!probe_read_access(buf, len)) {
+    goto access_violation;
+  }
+
+  return usb_hid_write(iface_num, buf, len);
+
+access_violation:
+  apptask_access_violation();
+  return 0;
+}
+
+int usb_hid_read_blocking__verified(uint8_t iface_num, uint8_t *buf,
+                                    uint32_t len, int timeout) {
+  if (!probe_write_access(buf, len)) {
+    goto access_violation;
+  }
+
+  return usb_hid_read_blocking(iface_num, buf, len, timeout);
+
+access_violation:
+  apptask_access_violation();
+  return 0;
+}
+
+int usb_hid_write_blocking__verified(uint8_t iface_num, const uint8_t *buf,
+                                     uint32_t len, int timeout) {
+  if (!probe_read_access(buf, len)) {
+    goto access_violation;
+  }
+
+  return usb_hid_write_blocking(iface_num, buf, len, timeout);
+
+access_violation:
+  apptask_access_violation();
+  return 0;
+}
+
+// ---------------------------------------------------------------------
+
+int usb_vcp_read__verified(uint8_t iface_num, uint8_t *buf, uint32_t len) {
+  if (!probe_write_access(buf, len)) {
+    goto access_violation;
+  }
+
+  return usb_vcp_read(iface_num, buf, len);
+
+access_violation:
+  apptask_access_violation();
+  return 0;
+}
+
+int usb_vcp_write__verified(uint8_t iface_num, const uint8_t *buf,
+                            uint32_t len) {
+  if (!probe_read_access(buf, len)) {
+    goto access_violation;
+  }
+
+  return usb_vcp_write(iface_num, buf, len);
+
+access_violation:
+  apptask_access_violation();
+  return 0;
+}
+
+int usb_vcp_read_blocking__verified(uint8_t iface_num, uint8_t *buf,
+                                    uint32_t len, int timeout) {
+  if (!probe_write_access(buf, len)) {
+    goto access_violation;
+  }
+
+  return usb_vcp_read_blocking(iface_num, buf, len, timeout);
+
+access_violation:
+  apptask_access_violation();
+  return 0;
+}
+
+int usb_vcp_write_blocking__verified(uint8_t iface_num, const uint8_t *buf,
+                                     uint32_t len, int timeout) {
+  if (!probe_read_access(buf, len)) {
+    goto access_violation;
+  }
+
+  return usb_vcp_write_blocking(iface_num, buf, len, timeout);
+
+access_violation:
+  apptask_access_violation();
+  return 0;
+}
+
+// ---------------------------------------------------------------------
+
+int usb_webusb_read__verified(uint8_t iface_num, uint8_t *buf, uint32_t len) {
+  if (!probe_write_access(buf, len)) {
+    goto access_violation;
+  }
+
+  return usb_webusb_read(iface_num, buf, len);
+
+access_violation:
+  apptask_access_violation();
+  return 0;
+}
+
+int usb_webusb_write__verified(uint8_t iface_num, const uint8_t *buf,
+                               uint32_t len) {
+  if (!probe_read_access(buf, len)) {
+    goto access_violation;
+  }
+
+  return usb_webusb_write(iface_num, buf, len);
+
+access_violation:
+  apptask_access_violation();
+  return 0;
+}
+
+int usb_webusb_read_blocking__verified(uint8_t iface_num, uint8_t *buf,
+                                       uint32_t len, int timeout) {
+  if (!probe_write_access(buf, len)) {
+    goto access_violation;
+  }
+
+  return usb_webusb_read_blocking(iface_num, buf, len, timeout);
+
+access_violation:
+  apptask_access_violation();
+  return 0;
+}
+
+int usb_webusb_write_blocking__verified(uint8_t iface_num, const uint8_t *buf,
+                                        uint32_t len, int timeout) {
+  if (!probe_read_access(buf, len)) {
+    goto access_violation;
+  }
+
+  return usb_webusb_write_blocking(iface_num, buf, len, timeout);
+
+access_violation:
+  apptask_access_violation();
+  return 0;
+}
+
+// ---------------------------------------------------------------------
+
+secbool __wur sdcard_read_blocks__verified(uint32_t *dest, uint32_t block_num,
+                                           uint32_t num_blocks) {
+  if (num_blocks >= (UINT32_MAX / SDCARD_BLOCK_SIZE)) {
+    goto access_violation;
+  }
+
+  if (!probe_write_access(dest, num_blocks * SDCARD_BLOCK_SIZE)) {
+    goto access_violation;
+  }
+
+  return sdcard_read_blocks(dest, block_num, num_blocks);
+
+access_violation:
+  apptask_access_violation();
+  return secfalse;
+}
+
+secbool __wur sdcard_write_blocks__verified(const uint32_t *src,
+                                            uint32_t block_num,
+                                            uint32_t num_blocks) {
+  if (num_blocks >= (UINT32_MAX / SDCARD_BLOCK_SIZE)) {
+    goto access_violation;
+  }
+
+  if (!probe_read_access(src, num_blocks * SDCARD_BLOCK_SIZE)) {
+    goto access_violation;
+  }
+
+  return sdcard_write_blocks(src, block_num, num_blocks);
+
+access_violation:
+  apptask_access_violation();
+  return secfalse;
+}
+
+// ---------------------------------------------------------------------
+
+bool __wur optiga_cert_size__verified(uint8_t index, size_t *cert_size) {
+  if (!probe_write_access(cert_size, sizeof(*cert_size))) {
+    goto access_violation;
+  }
+
+  return optiga_cert_size(index, cert_size);
+
+access_violation:
+  apptask_access_violation();
+  return false;
+}
+
+bool __wur optiga_read_cert__verified(uint8_t index, uint8_t *cert,
+                                      size_t max_cert_size, size_t *cert_size) {
+  if (!probe_write_access(cert, max_cert_size)) {
+    goto access_violation;
+  }
+
+  if (!probe_write_access(cert_size, sizeof(*cert_size))) {
+    goto access_violation;
+  }
+
+  return optiga_read_cert(index, cert, max_cert_size, cert_size);
+
+access_violation:
+  apptask_access_violation();
+  return false;
+}
+
+bool __wur optiga_read_sec__verified(uint8_t *sec) {
+  if (!probe_write_access(sec, sizeof(*sec))) {
+    goto access_violation;
+  }
+
+  return optiga_read_sec(sec);
+
+access_violation:
+  apptask_access_violation();
+  return false;
+}
+
+bool __wur optiga_random_buffer__verified(uint8_t *dest, size_t size) {
+  if (!probe_write_access(dest, size)) {
+    goto access_violation;
+  }
+
+  return optiga_random_buffer(dest, size);
+
+access_violation:
+  apptask_access_violation();
+  return false;
+}
+
+// ---------------------------------------------------------------------
+
+void storage_init__verified(PIN_UI_WAIT_CALLBACK callback, const uint8_t *salt,
+                            const uint16_t salt_len) {
+  if (!probe_read_access(salt, salt_len)) {
+    goto access_violation;
+  }
+
+  storage_init(callback, salt, salt_len);
+  return;
+
+access_violation:
+  apptask_access_violation();
+}
+
+secbool storage_unlock__verified(const uint8_t *pin, size_t pin_len,
+                                 const uint8_t *ext_salt) {
+  if (!probe_read_access(pin, pin_len)) {
+    goto access_violation;
+  }
+
+  if (!probe_read_access(ext_salt, EXTERNAL_SALT_SIZE)) {
+    goto access_violation;
+  }
+
+  return storage_unlock(pin, pin_len, ext_salt);
+
+access_violation:
+  apptask_access_violation();
+  return secfalse;
+}
+
+secbool storage_change_pin__verified(const uint8_t *oldpin, size_t oldpin_len,
+                                     const uint8_t *newpin, size_t newpin_len,
+                                     const uint8_t *old_ext_salt,
+                                     const uint8_t *new_ext_salt) {
+  if (!probe_read_access(oldpin, oldpin_len)) {
+    goto access_violation;
+  }
+
+  if (!probe_read_access(newpin, newpin_len)) {
+    goto access_violation;
+  }
+
+  if (!probe_read_access(old_ext_salt, EXTERNAL_SALT_SIZE)) {
+    goto access_violation;
+  }
+
+  if (!probe_read_access(new_ext_salt, EXTERNAL_SALT_SIZE)) {
+    goto access_violation;
+  }
+
+  return storage_change_pin(oldpin, oldpin_len, newpin, newpin_len,
+                            old_ext_salt, new_ext_salt);
+
+access_violation:
+  apptask_access_violation();
+  return secfalse;
+}
+
+void storage_ensure_not_wipe_code__verified(const uint8_t *pin,
+                                            size_t pin_len) {
+  if (!probe_read_access(pin, pin_len)) {
+    goto access_violation;
+  }
+
+  storage_ensure_not_wipe_code(pin, pin_len);
+  return;
+
+access_violation:
+  apptask_access_violation();
+}
+
+secbool storage_change_wipe_code__verified(const uint8_t *pin, size_t pin_len,
+                                           const uint8_t *ext_salt,
+                                           const uint8_t *wipe_code,
+                                           size_t wipe_code_len) {
+  if (!probe_read_access(pin, pin_len)) {
+    goto access_violation;
+  }
+
+  if (!probe_read_access(ext_salt, EXTERNAL_SALT_SIZE)) {
+    goto access_violation;
+  }
+
+  if (!probe_read_access(wipe_code, wipe_code_len)) {
+    goto access_violation;
+  }
+
+  return storage_change_wipe_code(pin, pin_len, ext_salt, wipe_code,
+                                  wipe_code_len);
+
+access_violation:
+  apptask_access_violation();
+  return secfalse;
+}
+
+secbool storage_get__verified(const uint16_t key, void *val,
+                              const uint16_t max_len, uint16_t *len) {
+  if (!probe_write_access(val, max_len)) {
+    goto access_violation;
+  }
+
+  if (!probe_write_access(len, sizeof(*len))) {
+    goto access_violation;
+  }
+
+  return storage_get(key, val, max_len, len);
+
+access_violation:
+  apptask_access_violation();
+  return secfalse;
+}
+
+secbool storage_set__verified(const uint16_t key, const void *val,
+                              const uint16_t len) {
+  if (!probe_read_access(val, len)) {
+    goto access_violation;
+  }
+
+  return storage_set(key, val, len);
+
+access_violation:
+  apptask_access_violation();
+  return secfalse;
+}
+
+secbool storage_next_counter__verified(const uint16_t key, uint32_t *count) {
+  if (!probe_write_access(count, sizeof(*count))) {
+    goto access_violation;
+  }
+
+  return storage_next_counter(key, count);
+
+access_violation:
+  apptask_access_violation();
+  return secfalse;
+}
+
+// ---------------------------------------------------------------------
+
+bool translations_write__verified(const uint8_t *data, uint32_t offset,
+                                  uint32_t len) {
+  if (!probe_read_access(data, len)) {
+    goto access_violation;
+  }
+
+  return translations_write(data, offset, len);
+
+access_violation:
+  apptask_access_violation();
+  return false;
+}
+
+const uint8_t *translations_read__verified(uint32_t *len, uint32_t offset) {
+  if (!probe_write_access(len, sizeof(*len))) {
+    goto access_violation;
+  }
+
+  return translations_read(len, offset);
+
+access_violation:
+  apptask_access_violation();
+  return NULL;
+}
+
+// ---------------------------------------------------------------------
+
+void entropy_get__verified(uint8_t *buf) {
+  if (!probe_write_access(buf, HW_ENTROPY_LEN)) {
+    goto access_violation;
+  }
+
+  entropy_get(buf);
+  return;
+
+access_violation:
+  apptask_access_violation();
+}
+
+// ---------------------------------------------------------------------
+
+secbool firmware_calc_hash__verified(const uint8_t *challenge,
+                                     size_t challenge_len, uint8_t *hash,
+                                     size_t hash_len,
+                                     firmware_hash_callback_t callback,
+                                     void *callback_context) {
+  if (!probe_read_access(challenge, challenge_len)) {
+    goto access_violation;
+  }
+
+  if (!probe_write_access(hash, hash_len)) {
+    goto access_violation;
+  }
+
+  return firmware_calc_hash(challenge, challenge_len, hash, hash_len, callback,
+                            callback_context);
+
+access_violation:
+  apptask_access_violation();
+  return secfalse;
+}
+
+secbool firmware_get_vendor__verified(char *buff, size_t buff_size) {
+  if (!probe_write_access(buff, buff_size)) {
+    goto access_violation;
+  }
+
+  return firmware_get_vendor(buff, buff_size);
+
+access_violation:
+  apptask_access_violation();
+  return secfalse;
+}
+
+#endif  // SYSCALL_DISPATCH
diff --git a/core/embed/trezorhal/stm32f4/syscall_verifiers.h b/core/embed/trezorhal/stm32f4/syscall_verifiers.h
new file mode 100644
index 0000000000..cdd9d1440c
--- /dev/null
+++ b/core/embed/trezorhal/stm32f4/syscall_verifiers.h
@@ -0,0 +1,169 @@
+/*
+ * This file is part of the Trezor project, https://trezor.io/
+ *
+ * Copyright (c) SatoshiLabs
+ *
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <http://www.gnu.org/licenses/>.
+ */
+
+#ifndef TREZORHAL_SYSCALL_VERIFIERS_H
+#define TREZORHAL_SYSCALL_VERIFIERS_H
+
+#ifdef SYSCALL_DISPATCH
+
+// ---------------------------------------------------------------------
+#include "systask.h"
+
+void system_exit__verified(int exit_code);
+
+void system_exit_error__verified(const char *title, size_t title_len,
+                                 const char *message, size_t message_len,
+                                 const char *footer, size_t footer_len);
+
+void system_exit_fatal__verified(const char *message, size_t message_len,
+                                 const char *file, size_t file_len, int line);
+
+// ---------------------------------------------------------------------
+#include "bootutils.h"
+
+void reboot_and_upgrade__verified(const uint8_t hash[32]);
+
+// ---------------------------------------------------------------------
+#include "display.h"
+
+#ifdef XFRAMEBUFFER
+bool display_get_frame_buffer__verified(display_fb_info_t *fb);
+#endif
+
+void display_fill__verified(const gfx_bitblt_t *bb);
+
+void display_copy_rgb565__verified(const gfx_bitblt_t *bb);
+
+// ---------------------------------------------------------------------
+#include "usb_hid.h"
+
+int usb_hid_read__verified(uint8_t iface_num, uint8_t *buf, uint32_t len);
+
+int usb_hid_write__verified(uint8_t iface_num, const uint8_t *buf,
+                            uint32_t len);
+
+int usb_hid_read_blocking__verified(uint8_t iface_num, uint8_t *buf,
+                                    uint32_t len, int timeout);
+int usb_hid_write_blocking__verified(uint8_t iface_num, const uint8_t *buf,
+                                     uint32_t len, int timeout);
+
+// ---------------------------------------------------------------------
+#include "usb_vcp.h"
+
+int usb_vcp_read__verified(uint8_t iface_num, uint8_t *buf, uint32_t len);
+
+int usb_vcp_write__verified(uint8_t iface_num, const uint8_t *buf,
+                            uint32_t len);
+
+int usb_vcp_read_blocking__verified(uint8_t iface_num, uint8_t *buf,
+                                    uint32_t len, int timeout);
+int usb_vcp_write_blocking__verified(uint8_t iface_num, const uint8_t *buf,
+                                     uint32_t len, int timeout);
+
+// ---------------------------------------------------------------------
+#include "usb_webusb.h"
+
+int usb_webusb_read__verified(uint8_t iface_num, uint8_t *buf, uint32_t len);
+
+int usb_webusb_write__verified(uint8_t iface_num, const uint8_t *buf,
+                               uint32_t len);
+
+int usb_webusb_read_blocking__verified(uint8_t iface_num, uint8_t *buf,
+                                       uint32_t len, int timeout);
+int usb_webusb_write_blocking__verified(uint8_t iface_num, const uint8_t *buf,
+                                        uint32_t len, int timeout);
+
+// ---------------------------------------------------------------------
+#include "sdcard.h"
+
+secbool __wur sdcard_read_blocks__verified(uint32_t *dest, uint32_t block_num,
+                                           uint32_t num_blocks);
+
+secbool __wur sdcard_write_blocks__verified(const uint32_t *src,
+                                            uint32_t block_num,
+                                            uint32_t num_blocks);
+
+// ---------------------------------------------------------------------
+#include "optiga.h"
+
+bool __wur optiga_cert_size__verified(uint8_t index, size_t *cert_size);
+
+bool __wur optiga_read_cert__verified(uint8_t index, uint8_t *cert,
+                                      size_t max_cert_size, size_t *cert_size);
+
+bool __wur optiga_read_sec__verified(uint8_t *sec);
+
+bool __wur optiga_random_buffer__verified(uint8_t *dest, size_t size);
+
+// ---------------------------------------------------------------------
+#include "storage.h"
+
+void storage_init__verified(PIN_UI_WAIT_CALLBACK callback, const uint8_t *salt,
+                            const uint16_t salt_len);
+
+secbool storage_unlock__verified(const uint8_t *pin, size_t pin_len,
+                                 const uint8_t *ext_salt);
+
+secbool storage_change_pin__verified(const uint8_t *oldpin, size_t oldpin_len,
+                                     const uint8_t *newpin, size_t newpin_len,
+                                     const uint8_t *old_ext_salt,
+                                     const uint8_t *new_ext_salt);
+
+void storage_ensure_not_wipe_code__verified(const uint8_t *pin, size_t pin_len);
+
+secbool storage_change_wipe_code__verified(const uint8_t *pin, size_t pin_len,
+                                           const uint8_t *ext_salt,
+                                           const uint8_t *wipe_code,
+                                           size_t wipe_code_len);
+
+secbool storage_get__verified(const uint16_t key, void *val,
+                              const uint16_t max_len, uint16_t *len);
+
+secbool storage_set__verified(const uint16_t key, const void *val,
+                              const uint16_t len);
+
+secbool storage_next_counter__verified(const uint16_t key, uint32_t *count);
+
+// ---------------------------------------------------------------------
+#include "translations.h"
+
+bool translations_write__verified(const uint8_t *data, uint32_t offset,
+                                  uint32_t len);
+
+const uint8_t *translations_read__verified(uint32_t *len, uint32_t offset);
+
+// ---------------------------------------------------------------------
+#include "entropy.h"
+
+void entropy_get__verified(uint8_t *buf);
+
+// ---------------------------------------------------------------------
+#include "fwutils.h"
+
+secbool firmware_calc_hash__verified(const uint8_t *challenge,
+                                     size_t challenge_len, uint8_t *hash,
+                                     size_t hash_len,
+                                     firmware_hash_callback_t callback,
+                                     void *callback_context);
+
+secbool firmware_get_vendor__verified(char *buff, size_t buff_size);
+
+#endif  // SYSCALL_DISPATCH
+
+#endif  // TREZORHAL_SYSCALL_VERIFIERS_H
diff --git a/core/embed/trezorhal/stm32f4/systask.c b/core/embed/trezorhal/stm32f4/systask.c
index 3528eb02ef..ec73670c1d 100644
--- a/core/embed/trezorhal/stm32f4/systask.c
+++ b/core/embed/trezorhal/stm32f4/systask.c
@@ -123,12 +123,14 @@ void systask_yield_to(systask_t* task) {
   systask_yield();
 }
 
-void systask_init(systask_t* task, uint32_t stack_ptr, uint32_t stack_size) {
+void systask_init(systask_t* task, uint32_t stack_ptr, uint32_t stack_size,
+                  void* applet) {
   memset(task, 0, sizeof(systask_t));
   task->sp = stack_ptr + stack_size;
   task->sp_lim = stack_ptr + 256;
   task->exc_return = 0xFFFFFFED;  // Thread mode, use PSP, pop FP context
   task->mpu_mode = MPU_MODE_APP;
+  task->applet = applet;
 }
 
 uint32_t* systask_push_data(systask_t* task, const void* data, size_t size) {
diff --git a/core/embed/trezorhal/stm32u5/syscall_probe.c b/core/embed/trezorhal/stm32u5/syscall_probe.c
new file mode 120000
index 0000000000..b9351466af
--- /dev/null
+++ b/core/embed/trezorhal/stm32u5/syscall_probe.c
@@ -0,0 +1 @@
+../stm32f4/syscall_probe.c
\ No newline at end of file
diff --git a/core/embed/trezorhal/stm32u5/syscall_probe.h b/core/embed/trezorhal/stm32u5/syscall_probe.h
new file mode 120000
index 0000000000..92b93e98c2
--- /dev/null
+++ b/core/embed/trezorhal/stm32u5/syscall_probe.h
@@ -0,0 +1 @@
+../stm32f4/syscall_probe.h
\ No newline at end of file
diff --git a/core/embed/trezorhal/stm32u5/syscall_verifiers.c b/core/embed/trezorhal/stm32u5/syscall_verifiers.c
new file mode 120000
index 0000000000..22b83e8c93
--- /dev/null
+++ b/core/embed/trezorhal/stm32u5/syscall_verifiers.c
@@ -0,0 +1 @@
+../stm32f4/syscall_verifiers.c
\ No newline at end of file
diff --git a/core/embed/trezorhal/stm32u5/syscall_verifiers.h b/core/embed/trezorhal/stm32u5/syscall_verifiers.h
new file mode 120000
index 0000000000..bd32627b4e
--- /dev/null
+++ b/core/embed/trezorhal/stm32u5/syscall_verifiers.h
@@ -0,0 +1 @@
+../stm32f4/syscall_verifiers.h
\ No newline at end of file
diff --git a/core/embed/trezorhal/systask.h b/core/embed/trezorhal/systask.h
index 58cfbe6abc..b802ec2f7c 100644
--- a/core/embed/trezorhal/systask.h
+++ b/core/embed/trezorhal/systask.h
@@ -117,6 +117,8 @@ typedef struct {
   mpu_mode_t mpu_mode;
   // Task post-mortem information
   systask_postmortem_t pminfo;
+  // Applet bound to the task
+  void* applet;
 
 } systask_t;
 
@@ -134,7 +136,8 @@ void systask_yield_to(systask_t* task);
 // Initializes a task with the given stack pointer, stack size
 //
 // The task must be not be running when the function is called
-void systask_init(systask_t* task, uint32_t stack_ptr, uint32_t stack_size);
+void systask_init(systask_t* task, uint32_t stack_ptr, uint32_t stack_size,
+                  void* context);
 
 // Pushes data onto the stack of the task
 //
diff --git a/core/site_scons/models/stm32f4_common.py b/core/site_scons/models/stm32f4_common.py
index 9e3b4cbe1a..2996479e80 100644
--- a/core/site_scons/models/stm32f4_common.py
+++ b/core/site_scons/models/stm32f4_common.py
@@ -56,7 +56,9 @@ def stm32f4_common_files(env, defines, sources, paths):
         "embed/trezorhal/stm32f4/secret.c",
         "embed/trezorhal/stm32f4/syscall.c",
         "embed/trezorhal/stm32f4/syscall_dispatch.c",
+        "embed/trezorhal/stm32f4/syscall_probe.c",
         "embed/trezorhal/stm32f4/syscall_stubs.c",
+        "embed/trezorhal/stm32f4/syscall_verifiers.c",
         "embed/trezorhal/stm32f4/system.c",
         "embed/trezorhal/stm32f4/systask.c",
         "embed/trezorhal/stm32f4/systick.c",
diff --git a/core/site_scons/models/stm32u5_common.py b/core/site_scons/models/stm32u5_common.py
index b69e88a324..f6d343033d 100644
--- a/core/site_scons/models/stm32u5_common.py
+++ b/core/site_scons/models/stm32u5_common.py
@@ -67,7 +67,9 @@ def stm32u5_common_files(env, defines, sources, paths):
         "embed/trezorhal/stm32u5/secure_aes.c",
         "embed/trezorhal/stm32u5/syscall.c",
         "embed/trezorhal/stm32u5/syscall_dispatch.c",
+        "embed/trezorhal/stm32u5/syscall_probe.c",
         "embed/trezorhal/stm32u5/syscall_stubs.c",
+        "embed/trezorhal/stm32u5/syscall_verifiers.c",
         "embed/trezorhal/stm32u5/system.c",
         "embed/trezorhal/stm32u5/systask.c",
         "embed/trezorhal/stm32u5/systick.c",