diff --git a/chb/api/XXPredicate.py b/chb/api/XXPredicate.py index 77536b7f..37cdca3f 100644 --- a/chb/api/XXPredicate.py +++ b/chb/api/XXPredicate.py @@ -4,7 +4,7 @@ # ------------------------------------------------------------------------------ # The MIT License (MIT) # -# Copyright (c) 2023 Aarno Labs LLC +# Copyright (c) 2023-2026 Aarno Labs LLC # # Permission is hereby granted, free of charge, to any person obtaining a copy # of this software and associated documentation files (the "Software"), to deal @@ -165,14 +165,38 @@ def is_xp_starts_thread(self) -> bool: def is_xp_tainted(self) -> bool: return False + @property + def is_xp_trusted_string(self) -> bool: + return False + + @property + def is_xp_trusted_os_cmd_string(self) -> bool: + return False + + @property + def is_xp_trusted_os_cmd_fmt_string(self) -> bool: + return False + + @property + def is_xp_trusted_os_cmd_fmt_arg_string(self) -> bool: + return False + @property def is_xp_validmem(self) -> bool: return False + @property + def is_xp_writes_string_from_fmt_string(self) -> bool: + return False + @property def is_xp_disjunction(self) -> bool: return False + @property + def is_xp_conditional(self) -> bool: + return False + @apiregistry.register_tag("ab", XXPredicate) class XXPAllocationBase(XXPredicate): @@ -925,15 +949,59 @@ def __str__(self) -> str: return "tainted(" + str(self.term) + ")" +@apiregistry.register_tag("ts", XXPredicate) +class XXTrustedString(XXPredicate): + + def __init__( + self, ixd: "InterfaceDictionary", ixval: IndexedTableValue) -> None: + XXPredicate.__init__(self, ixd, ixval) + + @property + def is_xp_trusted_string(self) -> bool: + return True + + @property + def term(self) -> "BTerm": + return self.id.bterm(self.args[0]) + + def __str__(self) -> str: + return "trusted-string(" + str(self.term) + ")" + + +@apiregistry.register_tag("tc", XXPredicate) +class XXTrustedOsCmdString(XXPredicate): + """String is safe to pass as an argument to system or popen.""" + + def __init__( + self, ixd: "InterfaceDictionary", ixval: IndexedTableValue) -> None: + XXPredicate.__init__(self, ixd, ixval) + + @property + def is_xp_trusted_os_cmd_string(self) -> bool: + return True + + @property + def term(self) -> "BTerm": + return self.id.bterm(self.args[0]) + + def __str__(self) -> str: + return "trusted-os-cmd-string(" + str(self.term) + ")" + + @apiregistry.register_tag("tfs", XXPredicate) class XXPTrustedOsCmdFmtString(XXPredicate): + """The string constructed by the format string is safe to pass to system. + + If a length is given, the string must evaluate to a value that has string + length less than the given length. + """ def __init__( self, ixd: "InterfaceDictionary", ixval: IndexedTableValue) -> None: XXPredicate.__init__(self, ixd, ixval) @property - def is_xp_trusted_os_cmd_string(self) -> bool: + def is_xp_trusted_os_cmd_fmt_string(self) -> bool: return True @property @@ -951,7 +1019,104 @@ def optlen(self) -> Optional["BTerm"]: return self.id.bterm(self.args[1]) def __str__(self) -> str: - return "trusted-os-cmd-fmt-string(" + str(self.fmt) + ", " + self.fmtkind + ", " + str(self.optlen) + ")" + return ( + "trusted-os-cmd-fmt-string(" + + str(self.fmt) + + ", " + + self.fmtkind + + ", " + + str(self.optlen) + + ")") + + +@apiregistry.register_tag("tfa", XXPredicate) +class XXPTrustedOsCmdFmtArgString(XXPredicate): + """String is safe to pass as a format argument to a string passed to system. + + It is safe if the format specifier associated with this argument is + enclosed in quotes according to the quotes property. + + If a length is given the length of the argument string must be less than + or equal to the given length. + """ + + def __init__( + self, ixd: "InterfaceDictionary", ixval: IndexedTableValue) -> None: + XXPredicate.__init__(self, ixd, ixval) + + @property + def is_xp_trusted_os_cmd_fmt_arg_string(self) -> bool: + return True + + @property + def fmt(self) -> "BTerm": + return self.id.bterm(self.args[0]) + + @property + def quotes(self) -> str: + return self.tags[1] + + @property + def optlen(self) -> Optional["BTerm"]: + if self.args[1] == -1: + return None + return self.id.bterm(self.args[1]) + + def __str__(self) -> str: + return ( + "trusted-os-cmd-fmt-string(" + + str(self.fmt) + + ", " + + self.quotes + + ", " + + str(self.optlen) + + ")") + + +@apiregistry.register_tag("wfs", XXPredicate) +class XXPWritesStringFromFmtString(XXPredicate): + """Side effect that asserts that a string is constructed from the given format string. + + An optional length imposes a maximum length on the string being written. + """ + + def __init__( + self, ixd: "InterfaceDictionary", ixval: IndexedTableValue) -> None: + XXPredicate.__init__(self, ixd, ixval) + + @property + def is_xp_writes_string_from_fmt_string(self) -> bool: + return True + + @property + def destination(self) -> "BTerm": + return self.id.bterm(self.args[0]) + + @property + def fmt(self) -> "BTerm": + return self.id.bterm(self.args[1]) + + @property + def fmtkind(self) -> str: + return self.tags[1] + + @property + def optlen(self) -> Optional["BTerm"]: + if self.args[2] == -1: + return None + return self.id.bterm(self.args[2]) + + def __str__(self) -> str: + return ( + "writes-string-from-fmt-string(" + + str(self.destination) + + ", " + + str(self.fmt) + + ", " + + self.fmtkind + + ", " + + str(self.optlen) + + ")") @apiregistry.register_tag("v", XXPredicate) diff --git a/chb/app/CHVersion.py b/chb/app/CHVersion.py index 8ee59334..23f57e87 100644 --- a/chb/app/CHVersion.py +++ b/chb/app/CHVersion.py @@ -1,3 +1,3 @@ chbversion: str = "0.3.0-20260527" -minimum_required_chb_version = "0.6.0_20260407" +minimum_required_chb_version = "0.6.0_20260527" diff --git a/chb/cmdline/AnalysisManager.py b/chb/cmdline/AnalysisManager.py index 6fc102f6..51708e10 100644 --- a/chb/cmdline/AnalysisManager.py +++ b/chb/cmdline/AnalysisManager.py @@ -75,6 +75,7 @@ def __init__( fns_no_lineq: List[str] = [], fns_exclude: List[str] = [], fns_include: List[str] = [], + fns_include_callees: bool = False, show_function_timing: bool = False, gc_compact: int = 0, lineq_instr_cutoff: int = 0, @@ -114,6 +115,7 @@ def __init__( self.fns_no_lineq = fns_no_lineq self.fns_exclude = fns_exclude self.fns_include = fns_include + self.fns_include_callees = fns_include_callees self.show_function_timing = show_function_timing self.gc_compact = gc_compact self.lineq_instr_cutoff = lineq_instr_cutoff @@ -483,6 +485,8 @@ def _analyze_until_stable( cmd.extend(["-fn_exclude", s]) for s in self.fns_include: cmd.extend(["-fn_include", s]) + if self.fns_include_callees: + cmd.append("-fn_include_callees") for s in self.specializations: cmd.extend(["-specialization", s]) if analysisrepeats > 1: diff --git a/chb/cmdline/chkx b/chb/cmdline/chkx index 4e352f29..4f6dcd21 100755 --- a/chb/cmdline/chkx +++ b/chb/cmdline/chkx @@ -476,6 +476,10 @@ def parse() -> argparse.Namespace: nargs="*", default=[], help="addresses of function to include in the analysis") + analyzecmd.add_argument( + "--fns_include_callees", + help="include callees of all fns_included", + action="store_true") analyzecmd.add_argument( "--analyze_all_named", help="include all functions named in userdata in the analysis", diff --git a/chb/cmdline/commandutil.py b/chb/cmdline/commandutil.py index 4cdf7761..d5082f29 100644 --- a/chb/cmdline/commandutil.py +++ b/chb/cmdline/commandutil.py @@ -416,6 +416,7 @@ def analyzecmd(args: argparse.Namespace) -> NoReturn: fns_no_lineq: List[str] = args.fns_no_lineq # function hex addresses fns_exclude: List[str] = args.fns_exclude # function hex addresses fns_include: List[str] = args.fns_include # function hex addresses + fns_include_callees: bool = args.fns_include_callees analyze_all_named: bool = args.analyze_all_named analyze_range_entry_points: List[str] = args.analyze_range_entry_points gc_compact: int = args.gc_compact @@ -553,6 +554,7 @@ def analyzecmd(args: argparse.Namespace) -> NoReturn: fns_no_lineq=fns_no_lineq, fns_exclude=fns_exclude, fns_include=fns_include, + fns_include_callees=fns_include_callees, gc_compact=gc_compact, show_function_timing=show_function_timing, lineq_instr_cutoff=lineq_instr_cutoff, diff --git a/chb/models/FunctionPrecondition.py b/chb/models/FunctionPrecondition.py index ec760ce4..140c4810 100644 --- a/chb/models/FunctionPrecondition.py +++ b/chb/models/FunctionPrecondition.py @@ -41,7 +41,7 @@ from chb.models.BTerm import BTerm, btermregistry from chb.models.ModelsType import ModelsType, mk_type - + import chb.util.fileutil as UF @@ -347,3 +347,29 @@ def __str__(self) -> str: + ", " + str(self.arg2) + ")") + + +@preconditionregistry.register_tag("trusted-os-cmd-string", FunctionPrecondition) +class PreTrustedOsCmdString(FunctionPrecondition): + + def __init__( + self, + fsem: "FunctionSemantics", + tag: str, + xnode: Optional[ET.Element] = None) -> None: + FunctionPrecondition.__init__(self, fsem, tag, xnode) + self._arg1: Optional[BTerm] = None + + @property + def arg1(self) -> BTerm: + if self._arg1 is None: + self._arg1 = ( + btermregistry.mk_instance(self.semantics, self.xterm(0), BTerm)) + return self._arg1 + + def __str__(self) -> str: + return ( + self.tag + + "(" + + str(self.arg1) + + ")") diff --git a/chb/models/ModelsAccess.py b/chb/models/ModelsAccess.py index a5a9dd5f..9d248b11 100644 --- a/chb/models/ModelsAccess.py +++ b/chb/models/ModelsAccess.py @@ -6,7 +6,7 @@ # # Copyright (c) 2016-2020 Kestrel Technology LLC # Copyright (c) 2020 Henny Sipma -# Copyright (c) 2021-2023 Aarno Labs LLC +# Copyright (c) 2021-2026 Aarno Labs LLC # # Permission is hereby granted, free of charge, to any person obtaining a copy # of this software and associated documentation files (the "Software"), to deal diff --git a/chb/summaries/bchsummaries.jar b/chb/summaries/bchsummaries.jar index 26ca2467..0bf72b52 100644 Binary files a/chb/summaries/bchsummaries.jar and b/chb/summaries/bchsummaries.jar differ