-
Notifications
You must be signed in to change notification settings - Fork 253
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Merge pull request #3 from kevinbackhouse/demos
QL Demos
- Loading branch information
Showing
105 changed files
with
3,901 additions
and
1 deletion.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1 +1,2 @@ | ||
.DS_Store | ||
*~ | ||
/.metadata/ |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1 @@ | ||
*.cache |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,12 @@ | ||
<?xml version="1.0" encoding="UTF-8"?> | ||
<projectDescription> | ||
<name>ql-demos-cpp</name> | ||
<comment></comment> | ||
<projects> | ||
</projects> | ||
<buildSpec> | ||
</buildSpec> | ||
<natures> | ||
<nature>com.semmle.plugin.qdt.core.qlnature</nature> | ||
</natures> | ||
</projectDescription> |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,10 @@ | ||
<?xml version="1.0" encoding="UTF-8" standalone="yes"?> | ||
<ns2:qlpath xmlns:ns2="https://semmle.com/schemas/qlpath"> | ||
<librarypath> | ||
<path kind="PLUGIN">com.semmle.code.cpp.library</path> | ||
</librarypath> | ||
<dbscheme kind="PLUGIN">com.semmle.code.cpp.dbscheme</dbscheme> | ||
<defaultImports> | ||
<defaultImport>cpp</defaultImport> | ||
</defaultImports> | ||
</ns2:qlpath> |
13 changes: 13 additions & 0 deletions
13
ql_demos/cpp/ChakraCore-bad-overflow-check/BadOverflowCheck.ql
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,13 @@ | ||
import cpp | ||
|
||
predicate isSmall(Expr e) { | ||
e.getType().getSize() < 4 | ||
} | ||
|
||
from AddExpr a, Variable v, RelationalOperation cmp | ||
where a.getAnOperand() = v.getAnAccess() | ||
and cmp.getAnOperand() = a | ||
and cmp.getAnOperand() = v.getAnAccess() | ||
and forall(Expr op | op = a.getAnOperand() | isSmall(op)) | ||
and not isSmall(a.getExplicitlyConverted()) | ||
select cmp, "Bad overflow check" |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,3 @@ | ||
Use [this snapshot](https://downloads.lgtm.com/snapshots/cpp/microsoft/chakracore/ChakraCore-revision-2017-April-12--18-13-26.zip) | ||
|
||
We now also have this query in our default suite: https://lgtm.com/rules/2156560627/ |
12 changes: 12 additions & 0 deletions
12
ql_demos/cpp/ChakraCore-bad-overflow-check/steps/01_overflow_checks.ql
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,12 @@ | ||
import cpp | ||
|
||
/** Matches `var < var + ???`. */ | ||
predicate overflowCheck(LocalScopeVariable var, AddExpr add, RelationalOperation compare) { | ||
compare.getAnOperand() = var.getAnAccess() and | ||
compare.getAnOperand() = add and | ||
add.getAnOperand() = var.getAnAccess() | ||
} | ||
|
||
from LocalScopeVariable var, AddExpr add | ||
where overflowCheck(var, add, _) | ||
select add, "Overflow check on variable of type " + var.getUnderlyingType() |
13 changes: 13 additions & 0 deletions
13
ql_demos/cpp/ChakraCore-bad-overflow-check/steps/02_var_size.ql
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,13 @@ | ||
import cpp | ||
|
||
/** Matches `var < var + ???`. */ | ||
predicate overflowCheck(LocalScopeVariable var, AddExpr add, RelationalOperation compare) { | ||
compare.getAnOperand() = var.getAnAccess() and | ||
compare.getAnOperand() = add and | ||
add.getAnOperand() = var.getAnAccess() | ||
} | ||
|
||
from LocalScopeVariable var, AddExpr add | ||
where overflowCheck(var, add, _) | ||
and var.getType().getSize() < 4 | ||
select add, "Overflow check on variable of type " + var.getUnderlyingType() |
14 changes: 14 additions & 0 deletions
14
ql_demos/cpp/ChakraCore-bad-overflow-check/steps/03_bad_overflow_check.ql
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,14 @@ | ||
import cpp | ||
|
||
/** Matches `var < var + ???`. */ | ||
predicate overflowCheck(LocalScopeVariable var, AddExpr add, RelationalOperation compare) { | ||
compare.getAnOperand() = var.getAnAccess() and | ||
compare.getAnOperand() = add and | ||
add.getAnOperand() = var.getAnAccess() | ||
} | ||
|
||
from LocalScopeVariable var, AddExpr add | ||
where overflowCheck(var, add, _) | ||
and var.getType().getSize() < 4 | ||
and not add.getConversion+().getType().getSize() < 4 | ||
select add, "Bad overflow check on variable of type " + var.getUnderlyingType() |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,57 @@ | ||
/** | ||
* @name Fizz Overflow | ||
* @description Narrowing conversions on untrusted data could enable | ||
* an attacker to trigger an integer overflow. | ||
* @kind path-problem | ||
* @problem.severity warning | ||
*/ | ||
|
||
import cpp | ||
import semmle.code.cpp.ir.dataflow.TaintTracking | ||
import semmle.code.cpp.ir.IR | ||
import DataFlow::PathGraph | ||
|
||
/** | ||
* The endianness conversion function `Endian::big()`. | ||
* It is Folly's replacement for `ntohs` and `ntohl`. | ||
*/ | ||
class EndianConvert extends Function { | ||
EndianConvert() { | ||
this.getName() = "big" and | ||
this.getDeclaringType().getName().matches("Endian") | ||
} | ||
} | ||
|
||
class Cfg extends TaintTracking::Configuration { | ||
Cfg() { this = "FizzOverflowIR" } | ||
|
||
/** Holds if `source` is a call to `Endian::big()`. */ | ||
override predicate isSource(DataFlow::Node source) { | ||
source | ||
.asInstruction() | ||
.(CallInstruction) | ||
.getCallTarget() | ||
.(FunctionInstruction) | ||
.getFunctionSymbol() instanceof EndianConvert | ||
} | ||
|
||
/** Holds if `sink` is a narrowing conversion. */ | ||
override predicate isSink(DataFlow::Node sink) { | ||
sink.asInstruction().getResultSize() < sink | ||
.asInstruction() | ||
.(ConvertInstruction) | ||
.getUnary() | ||
.getResultSize() | ||
} | ||
} | ||
|
||
from | ||
Cfg cfg, DataFlow::PathNode source, DataFlow::PathNode sink, ConvertInstruction conv, | ||
Type inputType, Type outputType | ||
where | ||
cfg.hasFlowPath(source, sink) and | ||
conv = sink.getNode().asInstruction() and | ||
inputType = conv.getUnary().getResultType() and | ||
outputType = conv.getResultType() | ||
select sink, source, sink, | ||
"Conversion of untrusted data from " + inputType + " to " + outputType + "." |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,5 @@ | ||
# Facebook Fizz integer overflow vulnerability (CVE-2019-3560) | ||
|
||
Use [this snapshot](https://downloads.lgtm.com/snapshots/cpp/facebook/fizz/facebookincubator_fizz_cpp-srcVersion_c69ad1baf3f04620393ebadc3eedd130b74f4023-dist_odasa-lgtm-2019-01-13-f9dca2a-universal.zip) for the demo. | ||
|
||
[Fizz](https://github.com/facebookincubator/fizz) contained a remotely triggerable infinite loop. For more details about the bug, see this [blog post](https://lgtm.com/blog/facebook_fizz_CVE-2019-3560). A proof-of-concept exploit is available [here](https://github.com/Semmle/SecurityExploits/tree/446048470633bf0f8da9570d008d056dbaa28ea9/Facebook/Fizz/CVE-2019-3560). |
12 changes: 12 additions & 0 deletions
12
ql_demos/cpp/Qualcomm-MSM-copy_from_user/00_copy_from_user.ql
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,12 @@ | ||
/** | ||
* @name Calls to copy_from_user | ||
* @description Find all calls to copy_from_user. | ||
*/ | ||
|
||
import cpp | ||
|
||
// This first query is essentially equivalent to `grep -r copy_from_user`. | ||
// It has almost 1300 results. | ||
from FunctionCall call | ||
where call.getTarget().getName() = "copy_from_user" | ||
select call |
25 changes: 25 additions & 0 deletions
25
ql_demos/cpp/Qualcomm-MSM-copy_from_user/01_copy_from_user_annotated.ql
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,25 @@ | ||
/** | ||
* @name Annotate with types and bounds | ||
* @description Find all calls to copy_from_user and annotates them with their | ||
* type and inferred size bounds. | ||
*/ | ||
|
||
import cpp | ||
import semmle.code.cpp.rangeanalysis.SimpleRangeAnalysis | ||
|
||
// Let's add some extra columns, so that we can see a bit more information | ||
// about the calls to copy_from_user. | ||
// | ||
// This shows that there are two fairly common patterns: | ||
// 1. copy_from_user into a statically sized buffer, and the | ||
// upper bound of `sizeArg` shows that it is safe. | ||
// 2. copy_from_user into a buffer that was allocated with kzalloc, | ||
// and the size argument of the kzalloc is the same as the | ||
// size argument of copy_from_user. These calls are safe. | ||
from FunctionCall call, Expr destArg, Expr sizeArg | ||
where | ||
call.getTarget().getName() = "copy_from_user" and | ||
destArg = call.getArgument(0) and | ||
sizeArg = call.getArgument(2) | ||
select call, destArg.getType(), lowerBound(sizeArg), upperBound(sizeArg), | ||
call.getFile().getRelativePath() |
24 changes: 24 additions & 0 deletions
24
ql_demos/cpp/Qualcomm-MSM-copy_from_user/02_filter_with_upperbound.ql
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,24 @@ | ||
/** | ||
* @name Filter with upper bound | ||
* @description This query excludes results that are safe because the upper | ||
* bound of the size argument is less than or equal to the size of | ||
* the destination variable. | ||
*/ | ||
|
||
import cpp | ||
import semmle.code.cpp.rangeanalysis.SimpleRangeAnalysis | ||
|
||
// Let's exclude filter out results that look like this: | ||
// | ||
// ``` | ||
// struct MyStruct s; | ||
// copy_from_user(&s, usrptr, sizeof(s)); | ||
// ``` | ||
from FunctionCall call, Expr destArg, Expr sizeArg | ||
where | ||
call.getTarget().getName() = "copy_from_user" and | ||
destArg = call.getArgument(0) and | ||
sizeArg = call.getArgument(2) and | ||
not destArg.getType().(PointerType).getBaseType().getSize() >= upperBound(sizeArg) | ||
select call, destArg.getType(), lowerBound(sizeArg), upperBound(sizeArg), | ||
call.getFile().getRelativePath() |
27 changes: 27 additions & 0 deletions
27
ql_demos/cpp/Qualcomm-MSM-copy_from_user/03_filter_with_upperbound.ql
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,27 @@ | ||
/** | ||
* @name Filter with upper bound, also for arrays | ||
* @description This query excludes results that are safe because the upper | ||
* bound of the size argument is less than or equal to the size of | ||
* the destination variable or array. | ||
*/ | ||
|
||
import cpp | ||
import semmle.code.cpp.rangeanalysis.SimpleRangeAnalysis | ||
|
||
// It turns out that the filter in the previous query does | ||
// not work for array types, so let's add a second filter which | ||
// excludes examples like this: | ||
// | ||
// ``` | ||
// struct MyStruct s[2]; | ||
// copy_from_user(s, usrptr, sizeof(s)); | ||
// ``` | ||
from FunctionCall call, Expr destArg, Expr sizeArg | ||
where | ||
call.getTarget().getName() = "copy_from_user" and | ||
destArg = call.getArgument(0) and | ||
sizeArg = call.getArgument(2) and | ||
not destArg.getType().(PointerType).getBaseType().getSize() >= upperBound(sizeArg) and | ||
not destArg.getType().(ArrayType).getSize() >= upperBound(sizeArg) | ||
select call, destArg.getType(), lowerBound(sizeArg), upperBound(sizeArg), | ||
call.getFile().getRelativePath() |
34 changes: 34 additions & 0 deletions
34
ql_demos/cpp/Qualcomm-MSM-copy_from_user/04_safe_malloc.ql
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,34 @@ | ||
/** | ||
* @name kzalloc only | ||
* @description If the copy_from_user is preceded by a kzalloc of the correct | ||
* size, then it is safe. To demonstrate, find only those results. | ||
*/ | ||
|
||
import cpp | ||
import semmle.code.cpp.valuenumbering.GlobalValueNumbering | ||
import semmle.code.cpp.dataflow.DataFlow | ||
|
||
// Let's see if we can detect this pattern: | ||
// | ||
// ``` | ||
// buf = kzalloc(size, GFP_KERNEL); | ||
// ... | ||
// copy_from_user(buf, usrptr, size); | ||
// ``` | ||
// | ||
// In the next query, we'll use `safe_malloc` to filter those | ||
// calls out, because they are safe. | ||
predicate safe_malloc(FunctionCall allocCall, FunctionCall copy_from_user) { | ||
exists(DataFlow::Node source, DataFlow::Node sink | | ||
allocCall.getTarget().getName() = "kzalloc" and | ||
copy_from_user.getTarget().getName() = "copy_from_user" and | ||
source.asExpr() = allocCall and | ||
sink.asExpr() = copy_from_user.getArgument(0) and | ||
DataFlow::localFlow(source, sink) and | ||
globalValueNumber(allocCall.getArgument(0)) = globalValueNumber(copy_from_user.getArgument(2)) | ||
) | ||
} | ||
|
||
from FunctionCall allocCall, FunctionCall copy_from_user | ||
where safe_malloc(allocCall, copy_from_user) | ||
select allocCall, copy_from_user |
37 changes: 37 additions & 0 deletions
37
ql_demos/cpp/Qualcomm-MSM-copy_from_user/05_filter_with_upperbound_and_safe_malloc.ql
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,37 @@ | ||
/** | ||
* @name Filter with upper bound and kzalloc | ||
* @description This query excludes results that are safe because the upper | ||
* bound of the size argument is less than or equal to the size of | ||
* the destination variable or array. It also excludes results | ||
* that are safe because the right amount of memory was allocated | ||
* with kzalloc. | ||
*/ | ||
|
||
import cpp | ||
import semmle.code.cpp.rangeanalysis.SimpleRangeAnalysis | ||
import semmle.code.cpp.valuenumbering.GlobalValueNumbering | ||
import semmle.code.cpp.dataflow.DataFlow | ||
|
||
// We wrote this predicate in the previous query. | ||
predicate safe_malloc(FunctionCall allocCall, FunctionCall copy_from_user) { | ||
exists(DataFlow::Node source, DataFlow::Node sink | | ||
allocCall.getTarget().getName() = "kzalloc" and | ||
copy_from_user.getTarget().getName() = "copy_from_user" and | ||
source.asExpr() = allocCall and | ||
sink.asExpr() = copy_from_user.getArgument(0) and | ||
DataFlow::localFlow(source, sink) and | ||
globalValueNumber(allocCall.getArgument(0)) = globalValueNumber(copy_from_user.getArgument(2)) | ||
) | ||
} | ||
|
||
// Add a filter to remove results that match the `safe_malloc` pattern. | ||
from FunctionCall call, Expr destArg, Expr sizeArg | ||
where | ||
call.getTarget().getName() = "copy_from_user" and | ||
destArg = call.getArgument(0) and | ||
sizeArg = call.getArgument(2) and | ||
not destArg.getType().(PointerType).getBaseType().getSize() >= upperBound(sizeArg) and | ||
not destArg.getType().(ArrayType).getSize() >= upperBound(sizeArg) and | ||
not safe_malloc(_, call) | ||
select call, destArg.getType(), lowerBound(sizeArg), upperBound(sizeArg), | ||
call.getFile().getRelativePath() |
43 changes: 43 additions & 0 deletions
43
ql_demos/cpp/Qualcomm-MSM-copy_from_user/06_stackaddress_dataflow.ql
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,43 @@ | ||
/** | ||
* @name Data flow from stack variable address | ||
* @description This restricts results to those that are most likely to be | ||
* dangerous: copying directly into a stack variable. | ||
* @kind path-problem | ||
* @problem.severity warning | ||
* @id demo/msm/06-stackaddress-dataflow | ||
*/ | ||
|
||
import cpp | ||
import semmle.code.cpp.rangeanalysis.SimpleRangeAnalysis | ||
import semmle.code.cpp.dataflow.DataFlow | ||
import DataFlow::PathGraph | ||
|
||
class Config extends DataFlow::Configuration { | ||
Config() { this = "copy_from_user" } | ||
|
||
override predicate isSource(DataFlow::Node source) { | ||
exists(LocalVariable v | source.asExpr().(AddressOfExpr).getOperand() = v.getAnAccess()) | ||
} | ||
|
||
override predicate isSink(DataFlow::Node sink) { | ||
// This is the logic that was previously in the select clause of the query. | ||
exists(FunctionCall call, Expr destArg, Expr sizeArg | | ||
call.getTarget().getName() = "copy_from_user" and | ||
destArg = sink.asExpr() and | ||
destArg = call.getArgument(0) and | ||
sizeArg = call.getArgument(2) and | ||
not destArg.getType().(PointerType).getBaseType().getSize() >= upperBound(sizeArg) and | ||
not destArg.getType().(ArrayType).getSize() >= upperBound(sizeArg) | ||
) | ||
} | ||
} | ||
|
||
// This query looks specifically for cases where the address of a local | ||
// variable is used as the target address of the `copy_from_user`. It also | ||
// uses the DataFlow library, so that you can use the path viewer to see | ||
// where the stack address comes from. | ||
// | ||
// The vulnerabilities are the final two results in `msm_cpp.c`. | ||
from Config cfg, DataFlow::PathNode source, DataFlow::PathNode sink | ||
where cfg.hasFlowPath(source, sink) | ||
select sink, source, sink, "possibly unsafe copy_from_user" |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,5 @@ | ||
[Blog post](https://lgtm.com/blog/qualcomm_copy_from_user) | ||
|
||
[Snapshot for this demo](https://downloads.lgtm.com/snapshots/cpp/qualcomm/msm/msm-4.4-revision-2017-May-07--08-33-56.zip) | ||
|
||
The blog post was written before we had the C++ dataflow library, so these demo queries are a bit different than the blog post. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1 @@ | ||
[snapshot](https://downloads.lgtm.com/snapshots/cpp/libssh2/libssh2_libssh2_C_C++_38bf7ce.zip) |
Oops, something went wrong.