AVR: Abstractly Verifying Reachability
417
set of specified resource limits, proof race initiates multiple AVR instances and
terminates execution as soon as one of these instances successfully races to the
result. Such a portfolio-based approach is crucial in practice for fast verification
performance since no single technique performs best in all cases [21,16]. It is
also further strengthened by complementing AVR’s word-level techniques with
state-of-the-art model checking engines like ABC dprove [14], IC3ia [23] etc.
4 Case Studies
1
4.1 Apache Buffer Overflow
We consider patched versions of two buffer overflow vulnerabilities [40] from
standard modules of the Apache web server [1].
apache-escape-absolute corrects a high severity vulnerability CVE2006-3747
[7] that fixes the out-of-bounds buffer overflow exploitation which allows a remote
attacker to cause a denial of service and execute arbitrary code via crafted URLs.
The patched version corrects a check (c < TOKEN SZ) to (c < TOKEN SZ − 1).
apache-get-tag fixes a medium severity vulnerability CVE-2004-0940 [6] that
exploits a buffer overflow when copying user-supplied tag strings into finite
buffers. A local attacker may leverage this issue to execute arbitrary code on
the affected computer with the privileges of the affected Apache server. The
patched version corrects a check that validates the length of the tag strings.
In less than a minute, AVR successfully verifies that both of these buffer
overflow exploits are unreachable in the patched versions for any buffer size.
AVR also provides human-readable proof certificates that are externally verified
using Z3, and provides provable assurance against these security vulnerabilities.
4.2 Public Key Authentication Protocol
The Needham-Schroeder public key authentication protocol [49] allows establishing mutual authentication between an initiator A and a responder B, after which
some session involving the exchange of messages between them can take place.
Unfortunately, this protocol is vulnerable to a man-in-the-middle attack [43]. If
an intruder I can persuade A to initiate a session with him, he can relay the
messages to B and convince B that he is communicating with A.
We consider an instance of the protocol from HWMCC’19 [17,52] with 3
initiators and responders each, and with an unsafe state defined as a responder
being finished authentication with the intruder as a party. Within a minute,
AVR finds an execution trace that establishes how to reach an unsafe state. The
counterexample witness produced by AVR can be replayed using the BtorSIM
simulator [4] to verify the execution trace and to debug the protocol.
4.3 Verifying Distributed Protocols
Beyond verifying model checking problems from finite domains, AVR has shown
preliminary application in the verification of distributed protocols, which are
1 All results presented in this paper can be replicated from [35,5].
417
set of specified resource limits, proof race initiates multiple AVR instances and
terminates execution as soon as one of these instances successfully races to the
result. Such a portfolio-based approach is crucial in practice for fast verification
performance since no single technique performs best in all cases [21,16]. It is
also further strengthened by complementing AVR’s word-level techniques with
state-of-the-art model checking engines like ABC dprove [14], IC3ia [23] etc.
4 Case Studies
1
4.1 Apache Buffer Overflow
We consider patched versions of two buffer overflow vulnerabilities [40] from
standard modules of the Apache web server [1].
apache-escape-absolute corrects a high severity vulnerability CVE2006-3747
[7] that fixes the out-of-bounds buffer overflow exploitation which allows a remote
attacker to cause a denial of service and execute arbitrary code via crafted URLs.
The patched version corrects a check (c < TOKEN SZ) to (c < TOKEN SZ − 1).
apache-get-tag fixes a medium severity vulnerability CVE-2004-0940 [6] that
exploits a buffer overflow when copying user-supplied tag strings into finite
buffers. A local attacker may leverage this issue to execute arbitrary code on
the affected computer with the privileges of the affected Apache server. The
patched version corrects a check that validates the length of the tag strings.
In less than a minute, AVR successfully verifies that both of these buffer
overflow exploits are unreachable in the patched versions for any buffer size.
AVR also provides human-readable proof certificates that are externally verified
using Z3, and provides provable assurance against these security vulnerabilities.
4.2 Public Key Authentication Protocol
The Needham-Schroeder public key authentication protocol [49] allows establishing mutual authentication between an initiator A and a responder B, after which
some session involving the exchange of messages between them can take place.
Unfortunately, this protocol is vulnerable to a man-in-the-middle attack [43]. If
an intruder I can persuade A to initiate a session with him, he can relay the
messages to B and convince B that he is communicating with A.
We consider an instance of the protocol from HWMCC’19 [17,52] with 3
initiators and responders each, and with an unsafe state defined as a responder
being finished authentication with the intruder as a party. Within a minute,
AVR finds an execution trace that establishes how to reach an unsafe state. The
counterexample witness produced by AVR can be replayed using the BtorSIM
simulator [4] to verify the execution trace and to debug the protocol.
4.3 Verifying Distributed Protocols
Beyond verifying model checking problems from finite domains, AVR has shown
preliminary application in the verification of distributed protocols, which are
1 All results presented in this paper can be replicated from [35,5].