_________     
   / __/__  /_____
  / /_  /_ </ ___/
 / __/___/ (__  ) 
/_/  /____/____/  

f3s

Format String Static Scanner is a static analysis tool for format string vulnerabilities in binaries.

• 1. About
  • 1.1. What does f3s do?
  • 1.2. Example usage
  • 1.3. What binary architectures are supported?
  • 1.4. What function sinks f3s looks for?
  • 1.5. What is a static taint analysis and how does it work?
  • 1.6. What static analyses and static binary techniques f3s makes use of?
  • 1.7. What is a format string vulnerability?
• 2. Dependencies and installation
• 3. Tests
• 4. Roadmap
• 5. Contributing
• 6. Acknowledgments
• 7. Meta

1. About

1.1. What does f3s do?

f3s makes use of a combination of static analyses directly on raw binaries to spot format string vulnerabilities.

A function (called sink) is flagged if the corresponding format parameter is found to be coming from user input.

For every flag it does also display a callstack trace of the path that brought from the starting top function to the vulnerability found.

f3s works on different types of architectures and stripped binaries.

1.2. Example usage

Use `-h` option to discover all other arguments.

1.3. What binary architectures are supported?

Currently f3s has been tested and works over these architectures:

• AMD64
• ARM32
• ARM64

1.4. What function sinks f3s looks for?

You can find and extend the checked functions with their respective parameters at ./src/sinks/fs_sinks.py. Here is the list of the currently ones present in the file

• printf
• fprintf
• sprintf
• dprintf
• snprintf
• vprintf
• vfprintf
• vdprintf
• vsprintf
• vsnprintf
• syslog

1.5. What is a static taint analysis and how does it work?

Static means it does not make use of running the binary to build knowledge out of it but rather just look at the machine code. There are few important concepts you should know about taint analysis:

• Taint: a taint is a flag that is logically associated with a particular datum. Tainted sources are usually user input arguments to a binary.
• Elaboration of tainted data: everything that touches taint gets tainted. So every output of every function that takes in tainted data will be tainted. This is tipically for keeping track of where the user input has flowed.
• Sink: a sink is a parameter of a possible vulnerable function. Usually function+parameter matches are pre-known and checked during the analysis
• Sink + Taint: when we find a sink that takes in a tainted value we know that our possible malicious data reached a possible vulnerable function and we trigger a report.

1.6. What static analyses and static binary techniques f3s makes use of?

• VEX intermediate representation included in angr to lift-up the binaries and operate with architecture agnostic code.
• Taint analysis for tainting input and reporting of sinks.
• Calling Convetion Analysis is made to asses the architecture of the binary and its calling convention.
• A Control Flow Graph Analysis is carried out to asses the presence of sinks and derive a set of callstack traces to it.
• A modified recursive Reaching Definition Analysis is laid out for every trace starting from the first top function and going forward towards the sink.
• A that point the Calling Convention, tainting of input and vulnerable sinks parameters are combined to asses if they will contain a tainted value.

1.7. What is a format string vulnerability?

printf("wow!")             //wow!!
printf("%s", "wow!")       //wow!
printf("%s %x", "wow!")    //wow! 0x4567B4AC    <-- stack content, information leakage!
printf("%s %2$x", "wow!")  //wow! 0x21776F77    <-- "wow!" string in stack after a offset of 2
printf("%s %2$n", "wow!")  //segmentation fault <-- selective memory corruption

When the format string "%x %x" is parsed the function expects two parameters, depending on the calling convention, in the stack. When these parameters are not supplied by the caller what was previously in the stack gets read. A special formatter %n could be used to write. If the user has control over the format string (e.g.: its supplied directly from input) it could craft it in such a wat to selectively leak and write arbitrarly information into the stack. This is a wikipedia article talking about format string vulnerability.

2. Dependencies and installation

In the file ./requirements.txt you can find a list of dependencies f3s relies on. You can install through pip with the command: pip install -r requirements.txt.

3. Tests

Under ./tests you can find a collection of ad-hoc made source codes to test and demonstrate the capabilities of f3s. To run all the tests do pytest run_tests.py.

⚠️ NOTE you should have gcc and both a ARM64 and ARM32 cross compiler installed in your systems to run the tests.

4. Roadmap

• Create f3s first version.
• Create a Docker image containing the toolbox and all the dependent software already setup
• Extend f3s also for command injection vulnerabilities

See the open issues for a full list of proposed features (and known issues).

5. Contributing

Contributions are more than welcome! Here's a short video tutorial on how to open a pull request.

6. Acknowledgments

• operation-mango in particular for the argument_resolver module
• pamplemousse in particular for its lecture video and blog post
• angr

7. Meta

gcsar

f3s by gcsar is licensed under CC BY-NC-SA 4.0

https://github.com/thisisnotgcsar