From 5a082ec3bb8fbf79fd702fd82f31781c166beb94 Mon Sep 17 00:00:00 2001 From: Dave Thaler Date: Mon, 1 Jan 2024 18:47:00 -0800 Subject: [PATCH] Fix checking of bad call parameter Prior to this change, if the caller didn't pass enough registers, the verifier would throw an exception instead of gracefully failing verification. Signed-off-by: Dave Thaler --- src/crab/ebpf_domain.cpp | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/src/crab/ebpf_domain.cpp b/src/crab/ebpf_domain.cpp index 90e920a17..d1ac9678d 100644 --- a/src/crab/ebpf_domain.cpp +++ b/src/crab/ebpf_domain.cpp @@ -2144,7 +2144,12 @@ void ebpf_domain_t::operator()(const Call& call) { case ArgPair::Kind::PTR_TO_WRITABLE_MEM: { bool store_numbers = true; - variable_t addr = get_type_offset_variable(param.mem).value(); + auto variable = get_type_offset_variable(param.mem); + if (!variable.has_value()) { + require(m_inv, linear_constraint_t::FALSE(), "Argument must be a pointer to writable memory"); + return; + } + variable_t addr = variable.value(); variable_t width = reg_pack(param.size).svalue; m_inv = type_inv.join_over_types(m_inv, param.mem, [&](NumAbsDomain& inv, type_encoding_t type) {