privileged operationsthat should only be accessible by
authorized users. To protect these privileged operations, these devices generally include some form of user verification. This verification almost always takes the form of an authentication of the user’s credentials before the privileged functionality is executed.
input determinism. Our authentication bypass model specifies that all paths leading from an entry point into the firmware to a privileged operation must validate some input that the attacker cannot derive from the firmware image itself or from prior communication with the device. In other words, we report an authentication bypass vulnerability when an attacker can craft inputs that lead the firmware execution to a privileged operation.
privileged operation, described by a security policy, and identifies a set of
privileged program points, which are points in the program that, if executed, represent the privileged operation being performed.
authentication slicefrom an entry point to the privileged program point.
privileged program point.
input determinismto determine whether the state in question represents the use of an authentication bypass vulnerability.
privileged program points. This set of program points is then utilized by Firmalice in its analysis to identify if the execution can reach the specified program point without proper authentication.
forced executionto systematically explore both directions of every conditional branch. When it encounters a computed or indirect jump, Firmalice can leverage its symbolic execute engine to reason about the possible targets of that jump.
def-usechains, in addition to
use-defchains, to optimize the worklist algorithm.
states. Whenever a path reaches the privileged program point, its associated state is labeled as a
privileged stateand passed to the Authentication Bypass Check module for further analysis, based on constraint solving.
initialization procedures. If an initialization procedure is identified, the state is duplicated: one state continues execution without modification, while the other one runs the initialization procedure before resuming execution.
privileged statefrom the Symbolic Execution engine, the Authentication Bypass Check module identifies the input and output from/to the user and reasons about the
exposureof data represented by the output. It then attempts to uniquely concretize the user input. If the user input can be uniquely concretized, then it represents that the input required to reach the
privileged program pointcan be uniquely determined by the attacker, and the associated path is labeled as an
authentication bypass. At this point, Firmalice terminates its analysis. In cases where the user input depends on data exposed by the device’s output, a function that can generate valid inputs for a provided output is produced.
exposedto the attacker. Specifically, this exposure does not just reveal information about the output data: information is also revealed about any data that depends on or is related to the output. The attackers can deduce information about authentication credentials by observing program outputs.