Application Verifier
Another freely available (and useful) Microsoft debugging tool is Application Verifier (www.microsoft.com/downloads). AppVerif effectively provides a verification layer between a running application and the operating system. This layer performs sanity checks on the data passed via Windows API calls, and also how the returned data is used. Common issues highlighted by using AppVerif include heap overruns, double freeing of heap allocations, memory leaks, using uninitialized critical sections, and double initialization of critical sections. Another useful feature is Low Resource Simulation, which simulates an application environment with low resources, such as when the system is under stress. Typically, this helps spot places in code where memory allocations are incorrectly assumed to always succeed.
Consider an example demonstrating the heap-checking feature of AppVerif. The C program in Example 5(a) allocates a 16-byte array and then fills the array using a for loop. However, the for loop contains a design error that results in a 1-byte buffer overrun. Despite this, the program compiles and runs successfully. However, when I configure AppVerif to verify this program and rerun it under the debugger, the debugger breaks in when it detects the AV caused by the buffer overrun. Once in the debugger, the stack command k gets the stack trace; see Example 5(b).
(a)
// t2.c
void main(void)
{
int i = 0;
char *p = 0;
p = (char *)malloc(16);
for (i=0; i<=16; i++)
{
// Buffer overrun when i=16
p[i] = (char)('a' + i);
}
}
(b)
0:000> k
ChildEBP RetAddr
0012ff80 004011d6 t2!main+0x45 [t2.c @ 11]
0012ffc0 7c816fd7 t2!mainCRTStartup+0xb4
0012fff0 00000000 kernel32!BaseProcessStart+0x2
To see the values of the local variables at the moment of the AV, I use the dv command, as in Example 6. This shows that the value of the index variable i is 16, and that the value of variable p is stored in memory address 0x0209eff0 and points to an array containing at least 16 characters. In this case, the value of p is displayed as a quoted string; however, this does not necessarily indicate that p points to a NULL-terminated string. One way to view the memory referenced by p is to issue the Display Memory as double-word values command dd. Example 6 also shows the results of the dd 0x0209eff0 command, which implies that the memory after the 16 bytes in the buffer corresponds to invalid memory (indicated by "?" characters). It also shows that the address immediately after these 16 bytes is 0x0209f000, which is the start of a new 4k block. To confirm whether memory is invalid, I can use the !address command as in Example 7. The results of !address 0x0209eff0 shows that the buffer referenced by p is PAGE_READWRITE memory, which is valid. The results of the command !address 0x0209f000 shows that the memory immediately following the 16-byte buffer is PAGE_NOACCESS memory. Writing into this PAGE_NOACCESS memory resulted in the AV.
0:000> dv
i = 16
p = 0x0209eff0 "abcdefghijklmnop"
0:000> dd 0x0209eff0
0209eff0 64636261 68676665 6c6b6a69 706f6e6d
0209f000 ???????? ???????? ???????? ????????
0209f010 ???????? ???????? ???????? ????????
0209f020 ???????? ???????? ???????? ????????
0:000> !address 0x0209eff0
02040000 : 0209e000 - 00001000
Type 00020000 MEM_PRIVATE
Protect 00000004 PAGE_READWRITE
State 00001000 MEM_COMMIT
Usage RegionUsagePageHeap
Handle 02041000
0:000> !address 0x0209f000
02040000 : 0209f000 - 000a1000
Type 00020000 MEM_PRIVATE
Protect 00000001 PAGE_NOACCESS
State 00001000 MEM_COMMIT
Usage RegionUsagePageHeap
Handle 02041000
When the code called malloc to allocate 16 bytes from the heap, AppVerif intercepted the call and allocated an entire valid block followed by an entire invalid block, and (here's the clever part) returned a pointer to only the last 16 bytes of the valid block. The result is that not only did our code attempt to step beyond the allocated buffer, but it also attempted to step into invalid memory. This attempt to access invalid memory triggered an exception that caused the debugger to break in. That is, AppVerif did not by itself find the buffer overrun. It instead set up the buffer so that Windows would trigger an exception when the buffer overrun occurred.
