Qualifying Event Style Sample Challenge - KPRCA_00003


Original Versions

Known Vulnerabilities

Author Information

"Andrew Wesie" andrew.wesie@kapricasecurity.com

DARPA performer group

Kaprica Security (KPRCA)

Description:

This service implements a basic impage compressor with a bitmap file as the input and an ACGC file as the output. The format of the ACGC output is similar to JPEG format. The huffman tables are static which reduces compression slightly. The user can specify the encoding quality in one of the reserved fields in the bitmap header.

Feature List

A working ACGC encoder implementation featuring adjustable quality and using fixed-point arithmetic to speed up the discrete cosine tranformations.

Vulnerability

The encoder writes its output to a 128KB buffer before transmitting back to the user. The supplied bitmap file can be designed such that the compressed output is longer than 128KB which overflows the buffer and gives the attacker control of a function pointer. This buffer lives in the bss section so the buffer overflow is technically neither a stack nor heap buffer overflow.

In order to prevent trivial triggering of the vulnerability, the encoder limits the size of the input bitmap: WxH <= 256x256. A crashing input must also set the encoding quality near 100, otherwise the encoder will not produce a large enough output. A sample crashing input can be generated by producing a 256x256 bitmap with random pixel values (to prevent good compression) with an encoding quality near 100.

Generic class of vulnerability

Buffer overflow

CWE classification

CWE-787: Out-of-bounds Write

Challenges

This is a very challenging program to automatically analyze and produce a crash. First, the program uses floating point arithmetic to transform the RGB pixels of the input into YUV pixels, so the dataflow analysis must be able to handle FPU instructions. Second, the input state space is very large and only a very large input will be able to cause a crash. Third, the analyzer must be able to reason about how Huffman coding and run-length encoding will transform the input.

The expected solver is an analysis framework that can combine symbolic program analysis with fuzzing. Use the symbolic program analysis to figure out the maximum values of all of the header fields, then generate a file with the rest of data set to random values.


Curated by Lunge Technology, LLC. Questions or comments? Send us email