Skip to main content

Using CodeQL variant analysis to find format string vulnerabilities - Part 2 ( Taint Analysis )

In our previous post we have seen examples on how we can perform simple analysis with codeql to detect format string vulnerabilities. There are couple of issues with the previous queries we wrote. Le us take an example where the data that is passed to a printf() call is hardcoded, hence the attacker has no control over it. In that case we would end up with too much of false positives. So this is where taint analysis will come useful. Here is the code that we are going to analyze here. 

 


Also let us try to exploit and see which are the scenarios in which they are vulnerable



So as per my input %08x.%08x , there are 3 cases where my input will cause a format string attack. So my model should be able to find these 3 paths that are potentially exploitable.
 
Next let us try to model taint flow of source to sink in which my source will be the user's input variable and my sink will be a flow where the user's input variable will be passed as the first parameter to the printf(user's input variable )


To write this query, I reused a part of the code from a stackoverflow question , 

https://stackoverflow.com/questions/58164464/semmle-ql-tainttracking-hasflow-problem-with-sources-that-taint-their-argumen

import cpp
import semmle.code.cpp.dataflow.TaintTracking
import DataFlow::PathGraph


predicate checkUserInput(Expr expr) {
    exists(FunctionCall fc, int i | verifythe2ndArgument(fc, i) and expr = fc.getArgument(i))
}
 
predicate verifythe2ndArgument(FunctionCall functionCall, int arg) {
    functionCall.getTarget().hasGlobalName("scanf") and
    arg = 1 // example, scanf("%s",userinput), userinput is being tainted here
}

class Config extends TaintTracking::Configuration {
    Config() { this = "Finding format string vulnerabilities" }
   
    override predicate isSource(DataFlow::Node source) {
        checkUserInput(source.asExpr())
        or
        checkUserInput(source.asDefiningArgument())
    }
    override predicate isSink(DataFlow::Node sink) {
        exists (FunctionCall fc | fc.getArgument(0)=sink.asExpr() and fc.getTarget().hasName("printf"))
  }
}

from Config cfg, DataFlow::PathNode source, DataFlow::PathNode sink
where cfg.hasFlowPath(source, sink)
select source.getNode().getLocation(), sink.getNode().getLocation(), "userinput flow to printf"


The query helps me to identify the same 3 potential location of format string vulnerability which we discussed above. The column [0] being the SOURCE and [1] being the SINK



Again this is not 100% fail proof as we only considered taking the tainted data from scanf input variable but not other possible input, or functions, etc. I will continue to improve the codeql query as I discover and learn more about it. Please let me know if you find any mistakes.

References

  • https://stackoverflow.com/questions/58164464/semmle-ql-tainttracking-hasflow-problem-with-sources-that-taint-their-argumen
  • https://help.semmle.com/QL/ql-training/cpp/data-flow-cpp.html#5

Popular posts from this blog

KringleCon : Sans Holiday Hack 2018 Writeup

SANS HOLIDAY HACK 2018 Writeup , KRINGLECON The objectives  Orientation Challenge  Directory Browsing  de Bruijn Sequences  Data Repo Analysis  AD Privilege Discovery  Badge Manipulation  HR Incident Response  Network Traffic Forensics  Ransomware Recovery  Who Is Behind It All? First I go to Bushy Evergreen and try to solve the terminal challenge . Solving it is fairly easy , Escape_Key followed by  ":q" without quotes After this we move to the kiosk and solve the questions The question were based on the themes of previous Holiday Hack Challenges. Once we answer it correctly we get the flag. For this I visited Minty Candycane and I tried to solve the terminal challenge.  The application has command injection vulnerability , so injecting a system command with the server ip allows execution of the command. So first I perform an `ls` operation to list of the directory contents , followed by a cat of t

Linux Privilege Escalation : SUID Binaries

After my OSCP Lab days are over I decided to do a little research and learn more on Privilege Escalation as it is my weak area.So over some series of blog post I am going to share with you some information of what I have learnt so far. The methods mentioned over here are not my own. This is something what I have learnt by reading articles, blogs and solving CTFs SUID - Set User ID The binaries which has suid enabled, runs with elevated privileges. Suppose you are logged in as non root user, but this suid bit enabled binaries can run with root privileges. How does a SUID Bit enable binary looks like ? -r- s r-x---  1 hack-me-bak-cracked hack-me-bak         7160 Aug 11  2015 bak How to find all the SUID enabled binaries ? hack-me-bak2@challenge02:~$ find / -perm -u=s 2>/dev/null /bin/su /bin/fusermount /bin/umount /usr/lib/openssh/ssh-keysign /usr/lib/eject/dmcrypt-get-device /usr/lib/dbus-1.0/dbus-daemon-launch-helper /usr/bin/gpasswd /usr/bin/newgrp /usr/bin

Bluetooth Low Energy : Build, Recon,Enumerate and Attack !

Introduction In this post I will try to share some information on bluetooth low energy protocol. Bluetooth Low Energy ( BLE ) is Bluetooth 4.0.It has been widely used in creating "smart" devices like bulbs that can be controlled by mobile apps, or electrical switches that can be controlled by mobile apps. The terms Low Energy refers to multiple distinctive features that is operating on low power and lower data transfer. Code BLE Internals and Working The next thing what we need to know is a profile. Now every bluetooth device can be categorized based on certain specification which makes it easy. Here we will take a close look into two profiles of Bluetooth which is specifically designed for BLE. Generic Access Profile (GAP) - This profiles describes how two BLE devices defines discovery and establishment of connection with each other. There are two types of data payload that can be used. The Advertising Data Payload and Scan Response Payload . The GAP uses br