From 9db52c7fa6f0bdf1ce77ee054aaa948d43d0d48e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Mon, 13 Apr 2026 19:56:27 +0200 Subject: [PATCH] fix: file read buffer overflow (#13392) This PR fixes a heap buffer overflow in `lean_io_prim_handle_read` that was triggered through an integer overflow in the size computation of an allocation. In addition it places several checked arithmetic operations on all relevant allocation paths to have potential future overflows be turned into crashes instead. The offending code now throws an out of memory error instead. Closes: #13388 --- src/include/lean/lean.h | 69 +++++++++++++++++++++++++-- src/runtime/compact.cpp | 14 +++--- src/runtime/io.cpp | 6 +++ src/runtime/mpz.cpp | 6 +-- src/runtime/object.cpp | 4 ++ src/runtime/uv/tcp.cpp | 3 ++ src/runtime/uv/udp.cpp | 3 ++ tests/compile/file_read_overflow.lean | 14 ++++++ 8 files changed, 104 insertions(+), 15 deletions(-) create mode 100644 tests/compile/file_read_overflow.lean diff --git a/src/include/lean/lean.h b/src/include/lean/lean.h index ffa0a1268e..9dcbe17aec 100644 --- a/src/include/lean/lean.h +++ b/src/include/lean/lean.h @@ -325,6 +325,55 @@ LEAN_EXPORT LEAN_NORETURN void lean_internal_panic(char const * msg); LEAN_EXPORT LEAN_NORETURN void lean_internal_panic_out_of_memory(void); LEAN_EXPORT LEAN_NORETURN void lean_internal_panic_unreachable(void); LEAN_EXPORT LEAN_NORETURN void lean_internal_panic_rc_overflow(void); +LEAN_EXPORT LEAN_NORETURN void lean_internal_panic_overflow(void); + +static inline bool lean_usize_mul_would_overflow(size_t a, size_t b) { +#if defined(__GNUC__) || defined(__clang__) + size_t r; + return __builtin_mul_overflow(a, b, &r); +#else + return a != 0 && b > SIZE_MAX / a; +#endif +} + +static inline bool lean_usize_add_would_overflow(size_t a, size_t b) { +#if defined(__GNUC__) || defined(__clang__) + size_t r; + return __builtin_add_overflow(a, b, &r); +#else + return a > SIZE_MAX - b; +#endif +} + +static inline size_t lean_usize_mul_checked(size_t a, size_t b) { +#if defined(__GNUC__) || defined(__clang__) + size_t r; + if (LEAN_UNLIKELY(__builtin_mul_overflow(a, b, &r))) { + lean_internal_panic_overflow(); + } + return r; +#else + if (a != 0 && b > SIZE_MAX / a) { + lean_internal_panic_overflow(); + } + return a * b; +#endif +} + +static inline size_t lean_usize_add_checked(size_t a, size_t b) { +#if defined(__GNUC__) || defined(__clang__) + size_t r; + if (LEAN_UNLIKELY(__builtin_add_overflow(a, b, &r))) { + lean_internal_panic_overflow(); + } + return r; +#else + if (a > SIZE_MAX - b) { + lean_internal_panic_overflow(); + } + return a + b; +#endif +} static inline size_t lean_align(size_t v, size_t a) { return (v / a)*a + a * (v % a != 0); @@ -617,7 +666,7 @@ static inline uint8_t * lean_ctor_scalar_cptr(lean_object * o) { static inline lean_object * lean_alloc_ctor(unsigned tag, unsigned num_objs, unsigned scalar_sz) { assert(tag <= LeanMaxCtorTag && num_objs < LEAN_MAX_CTOR_FIELDS && scalar_sz < LEAN_MAX_CTOR_SCALARS_SIZE); - lean_object * o = lean_alloc_ctor_memory(sizeof(lean_ctor_object) + sizeof(void*)*num_objs + scalar_sz); + lean_object * o = lean_alloc_ctor_memory(lean_usize_add_checked(lean_usize_add_checked(sizeof(lean_ctor_object), lean_usize_mul_checked(sizeof(void*), num_objs)), scalar_sz)); lean_set_st_header(o, tag, num_objs); return o; } @@ -727,7 +776,7 @@ static inline lean_object ** lean_closure_arg_cptr(lean_object * o) { return lea static inline lean_obj_res lean_alloc_closure(void * fun, unsigned arity, unsigned num_fixed) { assert(arity > 0); assert(num_fixed < arity); - lean_closure_object * o = (lean_closure_object*)lean_alloc_object(sizeof(lean_closure_object) + sizeof(void*)*num_fixed); + lean_closure_object * o = (lean_closure_object*)lean_alloc_object(lean_usize_add_checked(sizeof(lean_closure_object), lean_usize_mul_checked(sizeof(void*), num_fixed))); lean_set_st_header((lean_object*)o, LeanClosure, 0); o->m_fun = fun; o->m_arity = arity; @@ -773,7 +822,7 @@ LEAN_EXPORT lean_object* lean_apply_m(lean_object* f, unsigned n, lean_object** /* Arrays of objects (low level API) */ static inline lean_obj_res lean_alloc_array(size_t size, size_t capacity) { - lean_array_object * o = (lean_array_object*)lean_alloc_object(sizeof(lean_array_object) + sizeof(void*)*capacity); + lean_array_object * o = (lean_array_object*)lean_alloc_object(lean_usize_add_checked(sizeof(lean_array_object), lean_usize_mul_checked(sizeof(void*), capacity))); lean_set_st_header((lean_object*)o, LeanArray, 0); o->m_size = size; o->m_capacity = capacity; @@ -950,8 +999,18 @@ LEAN_EXPORT lean_object * lean_mk_array(lean_obj_arg n, lean_obj_arg v); /* Array of scalars */ +static inline bool lean_alloc_sarray_would_overflow(unsigned elem_size, size_t capacity) { + if (lean_usize_mul_would_overflow(elem_size, capacity)) { + return true; + } + if (lean_usize_add_would_overflow(sizeof(lean_sarray_object), elem_size * capacity)) { + return true; + } + return false; +} + static inline lean_obj_res lean_alloc_sarray(unsigned elem_size, size_t size, size_t capacity) { - lean_sarray_object * o = (lean_sarray_object*)lean_alloc_object(sizeof(lean_sarray_object) + elem_size*capacity); + lean_sarray_object * o = (lean_sarray_object*)lean_alloc_object(lean_usize_add_checked(sizeof(lean_sarray_object), lean_usize_mul_checked(elem_size, capacity))); lean_set_st_header((lean_object*)o, LeanScalarArray, elem_size); o->m_size = size; o->m_capacity = capacity; @@ -1113,7 +1172,7 @@ static inline lean_obj_res lean_float_array_set(lean_obj_arg a, b_lean_obj_arg i /* Strings */ static inline lean_obj_res lean_alloc_string(size_t size, size_t capacity, size_t len) { - lean_string_object * o = (lean_string_object*)lean_alloc_object(sizeof(lean_string_object) + capacity); + lean_string_object * o = (lean_string_object*)lean_alloc_object(lean_usize_add_checked(sizeof(lean_string_object), capacity)); lean_set_st_header((lean_object*)o, LeanString, 0); o->m_size = size; o->m_capacity = capacity; diff --git a/src/runtime/compact.cpp b/src/runtime/compact.cpp index 74b8b226dc..c8bf24aa82 100644 --- a/src/runtime/compact.cpp +++ b/src/runtime/compact.cpp @@ -143,7 +143,7 @@ object * object_compactor::copy_object(object * o) { void object_compactor::insert_sarray(object * o) { size_t sz = lean_sarray_size(o); unsigned elem_sz = lean_sarray_elem_size(o); - size_t obj_sz = sizeof(lean_sarray_object) + elem_sz*sz; + size_t obj_sz = lean_usize_add_checked(sizeof(lean_sarray_object), lean_usize_mul_checked(elem_sz, sz)); lean_sarray_object * new_o = (lean_sarray_object*)alloc(obj_sz); lean_set_non_heap_header_for_big((lean_object*)new_o, LeanScalarArray, elem_sz); new_o->m_size = sz; @@ -155,7 +155,7 @@ void object_compactor::insert_sarray(object * o) { void object_compactor::insert_string(object * o) { size_t sz = lean_string_size(o); size_t len = lean_string_len(o); - size_t obj_sz = sizeof(lean_string_object) + sz; + size_t obj_sz = lean_usize_add_checked(sizeof(lean_string_object), sz); lean_string_object * new_o = (lean_string_object*)alloc(obj_sz); lean_set_non_heap_header_for_big((lean_object*)new_o, LeanString, 0); new_o->m_size = sz; @@ -214,7 +214,7 @@ bool object_compactor::insert_array(object * o) { } if (missing_children) return false; - size_t obj_sz = sizeof(lean_array_object) + sizeof(void*)*sz; + size_t obj_sz = lean_usize_add_checked(sizeof(lean_array_object), lean_usize_mul_checked(sizeof(void*), sz)); lean_array_object * new_o = (lean_array_object*)alloc(obj_sz); lean_set_non_heap_header_for_big((lean_object*)new_o, LeanArray, 0); new_o->m_size = sz; @@ -274,8 +274,8 @@ bool object_compactor::insert_promise(object * o) { void object_compactor::insert_mpz(object * o) { #ifdef LEAN_USE_GMP size_t nlimbs = mpz_size(to_mpz(o)->m_value.m_val); - size_t data_sz = sizeof(mp_limb_t) * nlimbs; - size_t sz = sizeof(mpz_object) + data_sz; + size_t data_sz = lean_usize_mul_checked(sizeof(mp_limb_t), nlimbs); + size_t sz = lean_usize_add_checked(sizeof(mpz_object), data_sz); mpz_object * new_o = (mpz_object *)alloc(sz); memcpy(new_o, to_mpz(o), sizeof(mpz_object)); lean_set_non_heap_header((lean_object*)new_o, sz, LeanMPZ, 0); @@ -287,8 +287,8 @@ void object_compactor::insert_mpz(object * o) { m._mp_alloc = nlimbs; save(o, (lean_object*)new_o); #else - size_t data_sz = sizeof(mpn_digit) * to_mpz(o)->m_value.m_size; - size_t sz = sizeof(mpz_object) + data_sz; + size_t data_sz = lean_usize_mul_checked(sizeof(mpn_digit), to_mpz(o)->m_value.m_size); + size_t sz = lean_usize_add_checked(sizeof(mpz_object), data_sz); mpz_object * new_o = (mpz_object *)alloc(sz); // Manually copy the `mpz_object` to ensure `mpz` struct padding is left as // zero as prepared by `object_compactor::alloc`. `memcpy` would copy the diff --git a/src/runtime/io.cpp b/src/runtime/io.cpp index faad7c7631..f37250b0df 100644 --- a/src/runtime/io.cpp +++ b/src/runtime/io.cpp @@ -583,6 +583,9 @@ extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_truncate(b_obj_arg h) { /* Handle.read : (@& Handle) → USize → IO ByteArray */ extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_read(b_obj_arg h, usize nbytes) { FILE * fp = io_get_handle(h); + if (lean_alloc_sarray_would_overflow(1, nbytes)) { + return io_result_mk_error(decode_io_error(ENOMEM, NULL)); + } obj_res res = lean_alloc_sarray(1, 0, nbytes); if (nbytes == 0) { // std::fread doesn't handle 0 reads well, see https://github.com/leanprover/lean4/issues/12138 @@ -865,6 +868,9 @@ extern "C" LEAN_EXPORT obj_res lean_io_get_random_bytes (size_t nbytes) { } #endif + if (lean_alloc_sarray_would_overflow(1, nbytes)) { + return io_result_mk_error(decode_io_error(ENOMEM, NULL)); + } obj_res res = lean_alloc_sarray(1, 0, nbytes); size_t remain = nbytes; uint8_t *dst = lean_sarray_cptr(res); diff --git a/src/runtime/mpz.cpp b/src/runtime/mpz.cpp index 62bd0ab7bf..c255b3d355 100644 --- a/src/runtime/mpz.cpp +++ b/src/runtime/mpz.cpp @@ -340,7 +340,7 @@ static void mpz_dealloc(void *ptr, size_t size) { void mpz::allocate(size_t s) { m_size = s; - m_digits = static_cast(mpz_alloc(s * sizeof(mpn_digit))); + m_digits = static_cast(mpz_alloc(lean_usize_mul_checked(s, sizeof(mpn_digit)))); } void mpz::init() { @@ -409,8 +409,8 @@ void mpz::init_int64(int64 v) { void mpz::init_mpz(mpz const & v) { m_sign = v.m_sign; m_size = v.m_size; - m_digits = static_cast(mpz_alloc(m_size * sizeof(mpn_digit))); - memcpy(m_digits, v.m_digits, m_size * sizeof(mpn_digit)); + m_digits = static_cast(mpz_alloc(lean_usize_mul_checked(m_size, sizeof(mpn_digit)))); + memcpy(m_digits, v.m_digits, lean_usize_mul_checked(m_size, sizeof(mpn_digit))); } mpz::mpz() { diff --git a/src/runtime/object.cpp b/src/runtime/object.cpp index fb5a4484ee..3daddb1e30 100644 --- a/src/runtime/object.cpp +++ b/src/runtime/object.cpp @@ -106,6 +106,10 @@ extern "C" LEAN_EXPORT void lean_internal_panic_rc_overflow() { lean_internal_panic("reference counter overflowed"); } +extern "C" LEAN_EXPORT void lean_internal_panic_overflow() { + lean_internal_panic("integer overflow in runtime computation"); +} + bool g_exit_on_panic = false; bool g_panic_messages = true; diff --git a/src/runtime/uv/tcp.cpp b/src/runtime/uv/tcp.cpp index bd9f6026b0..761317fe6c 100644 --- a/src/runtime/uv/tcp.cpp +++ b/src/runtime/uv/tcp.cpp @@ -182,6 +182,9 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_send(b_obj_arg socket, obj_arg d } // Allocate buffer array for uv_write + if (lean_usize_mul_would_overflow(array_len, sizeof(uv_buf_t))) { + return lean_io_result_mk_error(decode_io_error(ENOMEM, nullptr)); + } uv_buf_t* bufs = (uv_buf_t*)malloc(array_len * sizeof(uv_buf_t)); for (size_t i = 0; i < array_len; i++) { diff --git a/src/runtime/uv/udp.cpp b/src/runtime/uv/udp.cpp index 5675bde4cc..284628989a 100644 --- a/src/runtime/uv/udp.cpp +++ b/src/runtime/uv/udp.cpp @@ -140,6 +140,9 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_send(b_obj_arg socket, obj_arg d return lean_io_result_mk_ok(promise); } + if (lean_usize_mul_would_overflow(array_len, sizeof(uv_buf_t))) { + return lean_io_result_mk_error(decode_io_error(ENOMEM, nullptr)); + } uv_buf_t* bufs = (uv_buf_t*)malloc(array_len * sizeof(uv_buf_t)); for (size_t i = 0; i < array_len; i++) { diff --git a/tests/compile/file_read_overflow.lean b/tests/compile/file_read_overflow.lean new file mode 100644 index 0000000000..ada0c8ddf6 --- /dev/null +++ b/tests/compile/file_read_overflow.lean @@ -0,0 +1,14 @@ +/-! +This issue is a minimal reproducer for #13388 which now throws an out of memory error. +-/ + +def main : IO UInt32 := do + let (h, _) ← IO.FS.createTempFile + let n : USize := (0 : USize) - (1 : USize) + try + discard <| h.read n + return 1 + catch e => + match e with + | .resourceExhausted .. => return 0 + | _ => return 1