From e8e72d57ca7d224a02f97ec337f0fe6910a8493c Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Mon, 29 Jun 2026 23:29:46 -0700 Subject: [PATCH 1/4] CHB: allow for formatstring in non-variadic function --- CodeHawk/CHB/bchlib/bCHARMFunctionInterface.ml | 9 +++------ 1 file changed, 3 insertions(+), 6 deletions(-) diff --git a/CodeHawk/CHB/bchlib/bCHARMFunctionInterface.ml b/CodeHawk/CHB/bchlib/bCHARMFunctionInterface.ml index 90b05399..aea5ef16 100644 --- a/CodeHawk/CHB/bchlib/bCHARMFunctionInterface.ml +++ b/CodeHawk/CHB/bchlib/bCHARMFunctionInterface.ml @@ -592,7 +592,8 @@ let arm_vfp_params __FILE__ __LINE__ ["fmtstringtype: " ^ (BCHFtsParameter.formatstring_type_to_string fmtstringtype); - "attr count: " ^ (string_of_int (List.length attrs))] in + "attr count: " ^ (string_of_int (List.length attrs)); + "varargs: " ^ (if varargs then "yes" else "no")] in fmtstringtype | _ -> NoFormat in let (_, _, params) = @@ -611,11 +612,7 @@ let arm_vfp_params | Ok btype, Ok tysize -> (* assume no packing at the argument top level *) let size = if tysize < 4 then 4 else tysize in - let fmt = - if varargs then - fmt index - else - NoFormat in + let fmt = fmt index in let (param, new_state) = if (is_int btype || is_pointer btype || is_enum btype) && size = 4 then get_arm_int_param_next_state ~fmt size name btype aa_state index From 15276b1a786b7ae0d0c9feaf9515deba8bced105 Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Mon, 29 Jun 2026 23:30:31 -0700 Subject: [PATCH 2/4] CHB: discharge trusted-os-cmd-fmt-arg-string condition --- .../bchlib/bCHAttributesFunctionSemantics.ml | 103 ++++++++++++------ CodeHawk/CHB/bchlib/bCHFunctionPODischarge.ml | 43 +++++++- CodeHawk/CHB/bchlib/bCHVersion.ml | 4 +- 3 files changed, 110 insertions(+), 40 deletions(-) diff --git a/CodeHawk/CHB/bchlib/bCHAttributesFunctionSemantics.ml b/CodeHawk/CHB/bchlib/bCHAttributesFunctionSemantics.ml index 06e02e35..3a9a12e2 100644 --- a/CodeHawk/CHB/bchlib/bCHAttributesFunctionSemantics.ml +++ b/CodeHawk/CHB/bchlib/bCHAttributesFunctionSemantics.ml @@ -351,6 +351,22 @@ let get_trusted_os_cmd_fmt_string_precondition attrparams_to_string "argparams" argparams] +let get_trusted_os_cmd_fmt_arg_string_precondition + (fparams: fts_parameter_t list) + (tagparams: b_attrparam_t list) + (argparams: b_attrparam_t list): xxpredicate_t traceresult = + match (tagparams, argparams) with + | ([ACons ("no_quotes", [])], [AInt refindex]) -> + let* par = get_par fparams refindex in + Ok (XXTrustedOsCmdFmtArgString (ArgValue par, NO_QUOTES, None)) + + | _ -> + Error [(elocm __LINE__) ^ "trusted_os_cmd_fmt_arg_string params not recognized"; + fparams_to_string fparams; + attrparams_to_string "tagparams" tagparams; + attrparams_to_string "argparams" argparams] + + let string_to_relational_op (s: string): relational_op_t traceresult = match s with | "eq" -> Ok PEquals @@ -490,6 +506,21 @@ let get_chk_pre_conditions (fparams: fts_parameter_t list) (attrparams: b_attrparam_t list): xxpredicate_t list = match attrparams with + + | (ACons ("allocation_base", tagparams)) :: argparams -> + TR.tfold + ~ok:(fun xpre -> [xpre]) + ~error:(fun e -> + begin + log_error_result + ~tag:"get_chk_preconditions:allocation_base" + ~msg:name + __FILE__ __LINE__ + [String.concat ", " e]; + [] + end) + (get_allocation_base_precondition fparams tagparams argparams) + | (ACons ("deref_read", tagparams)) :: argparams -> TR.tfold ~ok:(fun xpre -> [xpre]) @@ -532,173 +563,173 @@ let get_chk_pre_conditions end) (get_initialized_range_precondition fparams tagparams argparams) - | (ACons ("not_null", tagparams)) :: argparams -> + | (ACons ("input_format_string", tagparams)) :: argparams -> TR.tfold ~ok:(fun xpre -> [xpre]) ~error:(fun e -> begin log_error_result - ~tag:"get_chk_preconditions:not_null" + ~tag:"get_chk_preconditions:input_format_string" ~msg:name __FILE__ __LINE__ [String.concat ", " e]; [] end) - (get_not_null_precondition fparams tagparams argparams) + (get_input_format_string_precondition fparams tagparams argparams) - | (ACons ("null_terminated", tagparams)) :: argparams -> + | (ACons ("non_negative", tagparams)) :: argparams -> TR.tfold ~ok:(fun xpre -> [xpre]) ~error:(fun e -> begin log_error_result - ~tag:"get_chk_preconditions:null_terminated" + ~tag:"get_chk_preconditions:non_negative" ~msg:name __FILE__ __LINE__ [String.concat ", " e]; [] end) - (get_null_terminated_precondition fparams tagparams argparams) + (get_non_negative_precondition fparams tagparams argparams) - | (ACons ("output_format_string", tagparams)) :: argparams -> + | (ACons ("no_overlap", tagparams)) :: argparams -> TR.tfold ~ok:(fun xpre -> [xpre]) ~error:(fun e -> begin log_error_result - ~tag:"get_chk_preconditions:output_format_string" + ~tag:"get_chk_preconditions:no_overlap" ~msg:name __FILE__ __LINE__ [String.concat ", " e]; [] end) - (get_output_format_string_precondition fparams tagparams argparams) + (get_no_overlap_precondition fparams tagparams argparams) - | (ACons ("restricted_output_format_string", tagparams)) :: argparams -> + | (ACons ("not_null", tagparams)) :: argparams -> TR.tfold ~ok:(fun xpre -> [xpre]) ~error:(fun e -> begin log_error_result - ~tag:"get_chk_preconditions:restricted_output_format_string" + ~tag:"get_chk_preconditions:not_null" ~msg:name __FILE__ __LINE__ [String.concat ", " e]; [] end) - (get_restricted_output_format_string_precondition fparams tagparams argparams) + (get_not_null_precondition fparams tagparams argparams) - | (ACons ("trusted_os_cmd_fmt_string", tagparams)) :: argparams -> + | (ACons ("not_zero", tagparams)) :: argparams -> TR.tfold ~ok:(fun xpre -> [xpre]) ~error:(fun e -> begin log_error_result - ~tag:"get_chk_preconditions:trusted_os_cmd_fmt_string" + ~tag:"get_chk_preconditions:not_zero" ~msg:name __FILE__ __LINE__ [String.concat ", " e]; [] end) - (get_trusted_os_cmd_fmt_string_precondition fparams tagparams argparams) + (get_not_zero_precondition fparams tagparams argparams) - | (ACons ("input_format_string", tagparams)) :: argparams -> + | (ACons ("null_terminated", tagparams)) :: argparams -> TR.tfold ~ok:(fun xpre -> [xpre]) ~error:(fun e -> begin log_error_result - ~tag:"get_chk_preconditions:input_format_string" + ~tag:"get_chk_preconditions:null_terminated" ~msg:name __FILE__ __LINE__ [String.concat ", " e]; [] end) - (get_input_format_string_precondition fparams tagparams argparams) + (get_null_terminated_precondition fparams tagparams argparams) - | (ACons ("not_zero", tagparams)) :: argparams -> + | (ACons ("output_format_string", tagparams)) :: argparams -> TR.tfold ~ok:(fun xpre -> [xpre]) ~error:(fun e -> begin log_error_result - ~tag:"get_chk_preconditions:not_zero" + ~tag:"get_chk_preconditions:output_format_string" ~msg:name __FILE__ __LINE__ [String.concat ", " e]; [] end) - (get_not_zero_precondition fparams tagparams argparams) + (get_output_format_string_precondition fparams tagparams argparams) - | (ACons ("non_negative", tagparams)) :: argparams -> + | (ACons ("relational_expr", tagparams)) :: argparams -> TR.tfold ~ok:(fun xpre -> [xpre]) ~error:(fun e -> begin log_error_result - ~tag:"get_chk_preconditions:non_negative" + ~tag:"get_chk_preconditions:relational_expr" ~msg:name __FILE__ __LINE__ [String.concat ", " e]; [] end) - (get_non_negative_precondition fparams tagparams argparams) + (get_relational_expr_precondition fparams tagparams argparams) - | (ACons ("relational_expr", tagparams)) :: argparams -> + | (ACons ("restricted_output_format_string", tagparams)) :: argparams -> TR.tfold ~ok:(fun xpre -> [xpre]) ~error:(fun e -> begin log_error_result - ~tag:"get_chk_preconditions:relational_expr" + ~tag:"get_chk_preconditions:restricted_output_format_string" ~msg:name __FILE__ __LINE__ [String.concat ", " e]; [] end) - (get_relational_expr_precondition fparams tagparams argparams) + (get_restricted_output_format_string_precondition fparams tagparams argparams) - | (ACons ("no_overlap", tagparams)) :: argparams -> + | (ACons ("trusted_string", tagparams)) :: argparams -> TR.tfold ~ok:(fun xpre -> [xpre]) ~error:(fun e -> begin log_error_result - ~tag:"get_chk_preconditions:no_overlap" + ~tag:"get_chk_preconditions:trusted_string" ~msg:name __FILE__ __LINE__ [String.concat ", " e]; [] end) - (get_no_overlap_precondition fparams tagparams argparams) + (get_trusted_string_precondition fparams tagparams argparams) - | (ACons ("allocation_base", tagparams)) :: argparams -> + | (ACons ("trusted_os_cmd_fmt_arg_string", tagparams)) :: argparams -> TR.tfold ~ok:(fun xpre -> [xpre]) ~error:(fun e -> begin log_error_result - ~tag:"get_chk_preconditions:allocation_base" + ~tag:"get_chk_preconditions:trusted_os_cmd_fmt_arg_string" ~msg:name __FILE__ __LINE__ [String.concat ", " e]; [] end) - (get_allocation_base_precondition fparams tagparams argparams) + (get_trusted_os_cmd_fmt_arg_string_precondition fparams tagparams argparams) - | (ACons ("trusted_string", tagparams)) :: argparams -> + | (ACons ("trusted_os_cmd_fmt_string", tagparams)) :: argparams -> TR.tfold ~ok:(fun xpre -> [xpre]) ~error:(fun e -> begin log_error_result - ~tag:"get_chk_preconditions:trusted_string" + ~tag:"get_chk_preconditions:trusted_os_cmd_fmt_string" ~msg:name __FILE__ __LINE__ [String.concat ", " e]; [] end) - (get_trusted_string_precondition fparams tagparams argparams) + (get_trusted_os_cmd_fmt_string_precondition fparams tagparams argparams) | (ACons ("trusted_os_cmd_string", tagparams)) :: argparams -> TR.tfold diff --git a/CodeHawk/CHB/bchlib/bCHFunctionPODischarge.ml b/CodeHawk/CHB/bchlib/bCHFunctionPODischarge.ml index 6149fc05..cdff664f 100644 --- a/CodeHawk/CHB/bchlib/bCHFunctionPODischarge.ml +++ b/CodeHawk/CHB/bchlib/bCHFunctionPODischarge.ml @@ -334,7 +334,7 @@ let trusted_os_cmd_fmt_string_va_list_delegate | _ -> Open -let trusted_os_cmd_fmt_string_fmt_args_delegate +let trusted_os_cmd_fmt_string_fmt_args_delegate_local (finfo: function_info_int) (loc: location_int) (fmtargs: annotated_format_arg_t list): po_status_t = @@ -365,7 +365,7 @@ let discharge_trusted_os_cmd_fmt_string | VA_LIST -> trusted_os_cmd_fmt_string_va_list_delegate finfo loc x optlen | FMT_ARGS -> - trusted_os_cmd_fmt_string_fmt_args_delegate finfo loc fmtargs) + trusted_os_cmd_fmt_string_fmt_args_delegate_local finfo loc fmtargs) | _ -> status in match status with | Open -> @@ -506,6 +506,21 @@ let trusted_os_cmd_fmt_arg_string_parameter_postcondition ["x: " ^ (x2s x); "xpr do not match"]; Open end + | XXTainted bterm -> + if check_bterm bterm then + Violated ( + "postcondition of " + ^ ctinfo#get_name + ^ " states that value written may be tainted") + else + begin + log_diagnostics_result + ~tag + ~msg:(p2s loc#toPretty) + __FILE__ __LINE__ + ["x: " ^ (x2s x); "xpr do not match"]; + Open + end | p -> begin log_diagnostics_result @@ -549,6 +564,25 @@ let trusted_os_cmd_fmt_arg_string_delegate_local Open +let trusted_os_cmd_fmt_arg_string_delegate + (finfo: function_info_int) + (loc: location_int) + (xpr: xpr_t) + (quotes: quote_status_t) + (optlen: int option): po_status_t = + let floc = BCHFloc.get_finfo_floc finfo loc in + let xpxt_opt = floc#get_expression_externalizer in + match xpxt_opt with + | Some xpxt -> + (match xpxt#xpr_to_bterm BCHBCTypeUtil.t_charptr xpr with + | Some xfmtarg -> + let xpred = XXTrustedOsCmdFmtArgString (xfmtarg, quotes, optlen) in + let _ = finfo#add_precondition xpred in + Delegated (xpred) + | _ -> Open) + | _ -> Open + + let discharge_trusted_os_cmd_fmt_arg_string (finfo: function_info_int) (loc: location_int) @@ -569,6 +603,11 @@ let discharge_trusted_os_cmd_fmt_arg_string trusted_os_cmd_fmt_arg_string_parameter_postcondition finfo loc x quotes optlen | _ -> status in + let status = + match status with + | Open -> + trusted_os_cmd_fmt_arg_string_delegate finfo loc x quotes optlen + | _ -> status in let status = match status with | Open -> diff --git a/CodeHawk/CHB/bchlib/bCHVersion.ml b/CodeHawk/CHB/bchlib/bCHVersion.ml index 6d908fba..2cea2bf0 100644 --- a/CodeHawk/CHB/bchlib/bCHVersion.ml +++ b/CodeHawk/CHB/bchlib/bCHVersion.ml @@ -95,8 +95,8 @@ end let version = new version_info_t - ~version:"0.6.0_20260625" - ~date:"2026-06-25" + ~version:"0.6.0_20260629" + ~date:"2026-06-29" ~licensee: None ~maxfilesize: None () From c7a836c501240c3fe5e3477b310cdd38898aa21f Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Tue, 30 Jun 2026 09:56:30 -0700 Subject: [PATCH 3/4] CHB: add proof obligations for variadic format arguments --- CodeHawk/CHB/bchlib/bCHFloc.ml | 23 ++++++++++++++++++----- 1 file changed, 18 insertions(+), 5 deletions(-) diff --git a/CodeHawk/CHB/bchlib/bCHFloc.ml b/CodeHawk/CHB/bchlib/bCHFloc.ml index 43766f83..27b70b13 100644 --- a/CodeHawk/CHB/bchlib/bCHFloc.ml +++ b/CodeHawk/CHB/bchlib/bCHFloc.ml @@ -835,12 +835,12 @@ object (self) let fmtargs = fmtspec#get_arguments in let orig_npar = List.length (get_fts_parameters fintf) in let newfintf = add_format_spec_parameters fintf isinput fmtargs in + let new_pars = + List.filteri + (fun i _ -> i >= orig_npar) + (get_fts_parameters newfintf) in let new_sem = if isinput then - let new_pars = - List.filteri - (fun i _ -> i >= orig_npar) - (get_fts_parameters newfintf) in let new_ses = List.map (fun p -> match p.apar_type with @@ -856,7 +856,20 @@ object (self) {sem with fsem_sideeffects = sem.fsem_sideeffects @ new_ses} else - sem in + let new_preconditions = + List.fold_left (fun acc p -> + if is_char_pointer p.apar_type then + let argval = ArgValue p in + let ntp = ArgNullTerminatorPos argval in + let newpres = + [XXBuffer (t_char, argval, ntp); + XXInitializedRange (t_char, argval, ntp); + XXNullTerminated argval; + XXNotNull argval] in + newpres @ acc + else + acc) [] new_pars in + {sem with fsem_pre = sem.fsem_pre @ new_preconditions} in Some (newfintf, new_sem) else None From b55ee2afa3964dd1ec52e5e49650cbc245fb58c3 Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Tue, 30 Jun 2026 16:29:29 -0700 Subject: [PATCH 4/4] CHB: externalize stack parameters --- CodeHawk/CHB/bchlib/bCHFloc.ml | 41 +++++++++++++++++++-- CodeHawk/CHB/bchlib/bCHFunctionInterface.ml | 14 +++---- CodeHawk/CHB/bchlib/bCHFunctionSummary.ml | 9 ++--- CodeHawk/CHB/bchlib/bCHLibTypes.mli | 2 +- CodeHawk/CHB/bchlib/bCHVariable.ml | 2 +- 5 files changed, 51 insertions(+), 17 deletions(-) diff --git a/CodeHawk/CHB/bchlib/bCHFloc.ml b/CodeHawk/CHB/bchlib/bCHFloc.ml index 27b70b13..762e1ac9 100644 --- a/CodeHawk/CHB/bchlib/bCHFloc.ml +++ b/CodeHawk/CHB/bchlib/bCHFloc.ml @@ -208,6 +208,35 @@ object (self) None end) (finfo#env#get_initial_register_value_register v) + | XVar v when finfo#env#is_stack_parameter_value v -> + let indexopt = finfo#env#get_stack_parameter_index v in + (match indexopt with + | Some index -> + let _ = + finfo#update_summary + (finfo#get_summary#add_stack_parameter_location + (4 * index) btype 4) in + TR.tfold + ~ok:(fun ftspar -> Some (ArgValue ftspar)) + ~error:(fun e -> + begin + log_error_result + ~tag:"xpr_to_bterm" + __FILE__ __LINE__ + ["v: " ^ (p2s v#toPretty); + "index: " ^ (string_of_int index); + String.concat ", " e]; + None + end) + (finfo#get_summary#get_parameter_at_stack_offset (4 * index)) + | _ -> + begin + log_diagnostics_result + ~tag:"xpr_to_bterm:stack-parameter" + __FILE__ __LINE__ + ["xpr: " ^ (x2s xpr)]; + None + end) | XOp ((Xf "indexsize"), [xx]) -> let optt = self#xpr_to_bterm t_int xx in (match optt with @@ -268,9 +297,15 @@ object (self) self#finfo#update_summary (self#finfo#get_summary#add_stack_parameter_location (4 * index) btype 4) in - let ftspar = - self#finfo#get_summary#get_parameter_at_stack_offset (4 * index) in - Some (ArgValue ftspar) + TR.tfold + ~ok:(fun ftspar -> Some (ArgValue ftspar)) + ~error:(fun e -> + log_error_result + ~tag:"xpr_to_bterm" + __FILE__ __LINE__ + ["v: " ^ (p2s v#toPretty); String.concat ", " e]; + None) + (self#finfo#get_summary#get_parameter_at_stack_offset (4 * index)) | _ -> None) | XOp ((Xf "indexsize"), [xx]) -> let optt = self#xpr_to_bterm t_int xx in diff --git a/CodeHawk/CHB/bchlib/bCHFunctionInterface.ml b/CodeHawk/CHB/bchlib/bCHFunctionInterface.ml index 051c26fa..33ff1339 100644 --- a/CodeHawk/CHB/bchlib/bCHFunctionInterface.ml +++ b/CodeHawk/CHB/bchlib/bCHFunctionInterface.ml @@ -960,13 +960,13 @@ let add_function_stack_parameter_location loc :: fintf.fintf_parameter_locations in {fintf with fintf_parameter_locations = newlocations} | Some bctype -> - let _ = - chlog#add - "add-function-stack-parameter-location" - (LBLOCK [ - STR "Location not added; bctype is fixed: "; - STR (btype_to_string bctype)]) in - fintf + begin + log_diagnostics_result + ~tag:"add_function_stack_parameter_location: not added" + __FILE__ __LINE__ + ["fixed function type: " ^ (btype_to_string bctype)]; + fintf + end let add_function_global_parameter_location diff --git a/CodeHawk/CHB/bchlib/bCHFunctionSummary.ml b/CodeHawk/CHB/bchlib/bCHFunctionSummary.ml index f4cb5791..cf37f6fb 100644 --- a/CodeHawk/CHB/bchlib/bCHFunctionSummary.ml +++ b/CodeHawk/CHB/bchlib/bCHFunctionSummary.ml @@ -156,14 +156,13 @@ object (self:'a) Option.is_some (get_register_parameter_for_register self#get_function_interface reg) - method get_parameter_at_stack_offset (offset: int): fts_parameter_t = + method get_parameter_at_stack_offset (offset: int): fts_parameter_t traceresult = let spar = get_stack_parameter_at_offset self#get_function_interface offset in match spar with - | Some p -> p + | Some p -> Ok p | _ -> - raise - (BCH_failure - (LBLOCK [STR "Internal error: get_parameter_at_stack_offset"])) + Error [(elocm __LINE__) ^ "get_parameter_at_stack_offset"; + "offset: " ^ (string_of_int offset)] method get_returntype = get_fts_returntype self#get_function_interface diff --git a/CodeHawk/CHB/bchlib/bCHLibTypes.mli b/CodeHawk/CHB/bchlib/bCHLibTypes.mli index b5797194..b917c5d7 100644 --- a/CodeHawk/CHB/bchlib/bCHLibTypes.mli +++ b/CodeHawk/CHB/bchlib/bCHLibTypes.mli @@ -2551,7 +2551,7 @@ object ('a) method has_parameter_for_register: register_t -> bool - method get_parameter_at_stack_offset: int -> fts_parameter_t + method get_parameter_at_stack_offset: int -> fts_parameter_t traceresult method get_returntype: btype_t diff --git a/CodeHawk/CHB/bchlib/bCHVariable.ml b/CodeHawk/CHB/bchlib/bCHVariable.ml index 91b1d1bd..a1c4472e 100644 --- a/CodeHawk/CHB/bchlib/bCHVariable.ml +++ b/CodeHawk/CHB/bchlib/bCHVariable.ml @@ -785,7 +785,7 @@ object (self) tfold ~ok:(fun numoffset -> let four = mkNumerical 4 in - if numoffset#gt numerical_zero + if numoffset#geq numerical_zero && (numoffset#modulo four)#equal numerical_zero then Some ((numoffset#div four)#toInt) else