Skip to content

Commit 76146e4

Browse files
author
Nikita Kraiouchkine
committed
Refactor OutOfBounds.qll and arg/offset model
1 parent e9dd4a8 commit 76146e4

File tree

1 file changed

+70
-83
lines changed

1 file changed

+70
-83
lines changed

c/common/src/codingstandards/c/OutOfBounds.qll

Lines changed: 70 additions & 83 deletions
Original file line numberDiff line numberDiff line change
@@ -13,8 +13,6 @@ import codingstandards.cpp.PossiblyUnsafeStringOperation
1313
import codingstandards.cpp.SimpleRangeAnalysisCustomizations
1414
import semmle.code.cpp.dataflow.DataFlow
1515
import semmle.code.cpp.valuenumbering.GlobalValueNumbering
16-
import semmle.code.cpp.security.BufferAccess
17-
import semmle.code.cpp.security.BufferWrite
1816

1917
module OOB {
2018
bindingset[name, result]
@@ -588,47 +586,66 @@ module OOB {
588586
SimpleStringLibraryFunctionCall() { this.getTarget() instanceof SimpleStringLibraryFunction }
589587
}
590588

591-
int getStatedAllocValue(Expr e) {
592-
if upperBound(e) = exprMaxVal(e)
593-
then result = max(Expr source | DataFlow::localExprFlow(source, e) | source.getValue().toInt())
594-
else
595-
result =
596-
upperBound(e)
597-
.minimum(min(Expr source |
598-
DataFlow::localExprFlow(source, e)
599-
|
600-
source.getValue().toInt()
601-
))
589+
private Expr getSourceConstantExpr(Expr dest) {
590+
exists(result.getValue().toInt()) and
591+
DataFlow::localExprFlow(result, dest)
602592
}
603593

604-
int getStatedValue(Expr e) {
605-
result =
606-
upperBound(e)
607-
.minimum(min(Expr source | DataFlow::localExprFlow(source, e) | source.getValue().toInt()))
594+
/**
595+
* Gets the smallest of the upper bound of `e` or the largest source value (i.e. "stated value") that flows to `e`.
596+
* Because range-analysis can over-widen bounds, take the minimum of range analysis and data-flow sources.
597+
*
598+
* If there is no source value that flows to `e`, this predicate does not hold.
599+
*/
600+
private int getMaxStatedValue(Expr e) {
601+
result = upperBound(e).minimum(max(getSourceConstantExpr(e).getValue().toInt()))
602+
}
603+
604+
/**
605+
* Gets the smallest of the upper bound of `e` or the smallest source value (i.e. "stated value") that flows to `e`.
606+
* Because range-analysis can over-widen bounds, take the minimum of range analysis and data-flow sources.
607+
*
608+
* If there is no source value that flows to `e`, this predicate does not hold.
609+
*/
610+
private int getMinStatedValue(Expr e) {
611+
result = upperBound(e).minimum(min(getSourceConstantExpr(e).getValue().toInt()))
608612
}
609613

610614
/**
611615
* A class for reasoning about the offset of a variable from the original value flowing to it
612616
* as a result of arithmetic or pointer arithmetic expressions.
613617
*/
614-
int getArithmeticOperandStatedValue(Expr expr) {
615-
result = getStatedValue(expr.(PointerArithmeticExpr).getOperand())
618+
private int getArithmeticOffsetValue(Expr expr, Expr base) {
619+
result = getMinStatedValue(expr.(PointerArithmeticExpr).getOperand()) and
620+
base = expr.(PointerArithmeticExpr).getPointer()
616621
or
617622
// &(array[index]) expressions
618-
result = getStatedValue(expr.(AddressOfExpr).getOperand().(PointerArithmeticExpr).getOperand())
623+
result =
624+
getMinStatedValue(expr.(AddressOfExpr).getOperand().(PointerArithmeticExpr).getOperand()) and
625+
base = expr.(AddressOfExpr).getOperand().(PointerArithmeticExpr).getPointer()
626+
or
627+
result = getMinStatedValue(expr.(AddExpr).getRightOperand()) and
628+
base = expr.(AddExpr).getLeftOperand()
619629
or
620-
result = getStatedValue(expr.(BinaryArithmeticOperation).getRightOperand())
630+
result = -getMinStatedValue(expr.(SubExpr).getRightOperand()) and
631+
base = expr.(SubExpr).getLeftOperand()
621632
or
622-
expr instanceof IncrementOperation and result = 1
633+
expr instanceof IncrementOperation and
634+
result = 1 and
635+
base = expr.(IncrementOperation).getOperand()
623636
or
624-
expr instanceof DecrementOperation and result = -1
637+
expr instanceof DecrementOperation and
638+
result = -1 and
639+
base = expr.(DecrementOperation).getOperand()
625640
or
626641
// fall-back if `expr` is not an arithmetic or pointer arithmetic expression
627642
not expr instanceof PointerArithmeticExpr and
628643
not expr.(AddressOfExpr).getOperand() instanceof PointerArithmeticExpr and
629-
not expr instanceof BinaryArithmeticOperation and
644+
not expr instanceof AddExpr and
645+
not expr instanceof SubExpr and
630646
not expr instanceof IncrementOperation and
631647
not expr instanceof DecrementOperation and
648+
base = expr and
632649
result = 0
633650
}
634651

@@ -660,8 +677,9 @@ module OOB {
660677
abstract predicate isNotNullTerminated();
661678
}
662679

663-
class DynamicAllocationSource extends PointerToObjectSource instanceof AllocationExpr,
664-
FunctionCall {
680+
private class DynamicAllocationSource extends PointerToObjectSource instanceof AllocationExpr,
681+
FunctionCall
682+
{
665683
DynamicAllocationSource() {
666684
// exclude OperatorNewAllocationFunction to only deal with raw malloc-style calls,
667685
// which do not apply a multiple to the size of the allocation passed to them.
@@ -742,7 +760,7 @@ module OOB {
742760
)
743761
}
744762

745-
override int getFixedSize() { result = getStatedAllocValue(getSizeExpr()) }
763+
override int getFixedSize() { result = getMaxStatedValue(getSizeExpr()) }
746764

747765
override predicate isNotNullTerminated() { none() }
748766
}
@@ -751,7 +769,7 @@ module OOB {
751769
* A `PointerToObjectSource` which is an `AddressOfExpr` to a variable
752770
* that is not a field or pointer type.
753771
*/
754-
class AddressOfExprSource extends PointerToObjectSource instanceof AddressOfExpr {
772+
private class AddressOfExprSource extends PointerToObjectSource instanceof AddressOfExpr {
755773
AddressOfExprSource() {
756774
exists(Variable v |
757775
v = this.getOperand().(VariableAccess).getTarget() and
@@ -774,7 +792,7 @@ module OOB {
774792
/**
775793
* A `PointerToObjectSource` which is a `VariableAccess` to a static buffer
776794
*/
777-
class StaticBufferAccessSource extends PointerToObjectSource instanceof VariableAccess {
795+
private class StaticBufferAccessSource extends PointerToObjectSource instanceof VariableAccess {
778796
StaticBufferAccessSource() {
779797
not this.getTarget() instanceof Field and
780798
not this.getTarget().getUnspecifiedType() instanceof PointerType and
@@ -809,16 +827,6 @@ module OOB {
809827
) and
810828
not this.(VariableAccess).getTarget() instanceof GlobalVariable and
811829
not exists(this.(VariableAccess).getTarget().getInitializer()) and
812-
not exists(FunctionCall memset, Expr destBuffer |
813-
(
814-
destBuffer = memset.(MemsetBA).getBuffer(_, _)
815-
or
816-
memset.getTarget().getName() = getNameOrInternalName("memset") and
817-
destBuffer = memset.getArgument(0)
818-
) and
819-
memset.getArgument(1).getValue().toInt() = 0 and
820-
this.(VariableAccess).getTarget().getAnAccess() = destBuffer
821-
) and
822830
// exclude any BufferAccessLibraryFunction that writes to the buffer and does not require
823831
// a null-terminated buffer argument for its write argument
824832
not exists(
@@ -845,7 +853,7 @@ module OOB {
845853
* A `PointerToObjectSource` which is a string literal that is not
846854
* part of an variable initializer (to deduplicate `StaticBufferAccessSource`)
847855
*/
848-
class StringLiteralSource extends PointerToObjectSource instanceof StringLiteral {
856+
private class StringLiteralSource extends PointerToObjectSource instanceof StringLiteral {
849857
StringLiteralSource() { not this instanceof CharArrayInitializedWithStringLiteral }
850858

851859
override Expr getPointer() { result = this }
@@ -862,7 +870,7 @@ module OOB {
862870
override predicate isNotNullTerminated() { none() }
863871
}
864872

865-
class PointerToObjectSourceOrSizeToBufferAccessFunctionConfig extends DataFlow::Configuration {
873+
private class PointerToObjectSourceOrSizeToBufferAccessFunctionConfig extends DataFlow::Configuration {
866874
PointerToObjectSourceOrSizeToBufferAccessFunctionConfig() {
867875
this = "PointerToObjectSourceOrSizeToBufferAccessFunctionConfig"
868876
}
@@ -883,10 +891,8 @@ module OOB {
883891
arg = ba.getARelevantExpr()
884892
) and
885893
(
886-
sink.asExpr() = arg
887-
or
888-
getArithmeticOffsetValue(arg) > 0 and
889-
sink.asExpr() = arg.getAChild*()
894+
sink.asExpr() = arg or
895+
exists(getArithmeticOffsetValue(arg, sink.asExpr()))
890896
)
891897
)
892898
}
@@ -910,58 +916,35 @@ module OOB {
910916
}
911917
}
912918

913-
predicate hasFlowFromBufferOrSizeExprToUse(Expr source, Expr use) {
919+
private predicate hasFlowFromBufferOrSizeExprToUse(Expr source, Expr use) {
914920
exists(PointerToObjectSourceOrSizeToBufferAccessFunctionConfig config, Expr useOrChild |
915-
(
916-
useOrChild = use
917-
or
918-
getArithmeticOffsetValue(use) > 0 and
919-
useOrChild = use.getAChild*()
920-
) and
921+
exists(getArithmeticOffsetValue(use, useOrChild)) and
921922
config.hasFlow(DataFlow::exprNode(source), DataFlow::exprNode(useOrChild))
922923
)
923924
}
924925

925-
predicate bufferUseComputableBufferSize(Expr bufferUse, Expr source, int size) {
926+
private predicate bufferUseComputableBufferSize(Expr bufferUse, Expr source, int size) {
926927
// flow from a PointerToObjectSource for which we can compute the exact size
927928
size = source.(PointerToObjectSource).getFixedSize() and
928929
hasFlowFromBufferOrSizeExprToUse(source, bufferUse)
929930
}
930931

931-
predicate bufferUseNonComputableSize(Expr bufferUse, Expr source) {
932+
private predicate bufferUseNonComputableSize(Expr bufferUse, Expr source) {
932933
not bufferUseComputableBufferSize(bufferUse, source, _) and
933934
hasFlowFromBufferOrSizeExprToUse(source.(DynamicAllocationSource), bufferUse)
934935
}
935936

936-
predicate sizeExprComputableSize(Expr sizeExpr, Expr source, int size) {
937+
private predicate sizeExprComputableSize(Expr sizeExpr, Expr source, int size) {
937938
// computable direct value
938-
size = getStatedValue(sizeExpr) and
939+
size = getMinStatedValue(sizeExpr) and
939940
source = sizeExpr
940941
or
941942
// computable source value that flows to the size expression
942-
size = source.(DynamicAllocationSource).getFixedSize() + getArithmeticOffsetValue(sizeExpr) and
943+
size = source.(DynamicAllocationSource).getFixedSize() + getArithmeticOffsetValue(sizeExpr, _) and
943944
hasFlowFromBufferOrSizeExprToUse(source.(DynamicAllocationSource).getSizeExprSource(_, _),
944945
sizeExpr)
945946
}
946947

947-
int getArithmeticOffsetValue(Expr expr) {
948-
result = getStatedValue(expr.(PointerArithmeticExpr).getOperand())
949-
or
950-
// edge-case: &(array[index]) expressions
951-
result = getStatedValue(expr.(AddressOfExpr).getOperand().(PointerArithmeticExpr).getOperand())
952-
or
953-
// AddExpr
954-
result = getStatedValue(expr.(AddExpr).getAnOperand())
955-
or
956-
// SubExpr
957-
result = -getStatedValue(expr.(SubExpr).getAnOperand())
958-
or
959-
// fall-back
960-
not expr instanceof PointerArithmeticExpr and
961-
not expr.(AddressOfExpr).getOperand() instanceof PointerArithmeticExpr and
962-
result = 0
963-
}
964-
965948
/**
966949
* If the size is not computable locally, then it is either:
967950
*
@@ -1012,12 +995,16 @@ module OOB {
1012995
readBuffer = fc.getReadArg() and
1013996
writeBuffer = fc.getWriteArg() and
1014997
exists(int readSizeMult, int writeSizeMult, int readBufferSizeBase, int writeBufferSizeBase |
998+
// the read and write buffer sizes must be derived from computable constants
1015999
bufferUseComputableBufferSize(readBuffer, _, readBufferSizeBase) and
10161000
bufferUseComputableBufferSize(writeBuffer, _, writeBufferSizeBase) and
1001+
// calculate the buffer byte sizes (size base is the number of elements)
10171002
readSizeMult = fc.getReadSizeArgMult() and
10181003
writeSizeMult = fc.getWriteSizeArgMult() and
1019-
readBufferSize = readBufferSizeBase - readSizeMult * getArithmeticOffsetValue(readBuffer) and
1020-
writeBufferSize = writeBufferSizeBase - writeSizeMult * getArithmeticOffsetValue(writeBuffer) and
1004+
readBufferSize = readBufferSizeBase - readSizeMult * getArithmeticOffsetValue(readBuffer, _) and
1005+
writeBufferSize =
1006+
writeBufferSizeBase - writeSizeMult * getArithmeticOffsetValue(writeBuffer, _) and
1007+
// the read buffer size is larger than the write buffer size
10211008
readBufferSize > writeBufferSize and
10221009
(
10231010
// if a size arg exists and it is computable, then it must be <= to the write buffer size
@@ -1051,7 +1038,7 @@ module OOB {
10511038
// If the bufferArg is an access of a static buffer, do not look for "long distance" sources
10521039
(bufferArg instanceof StaticBufferAccessSource implies bufferSource = bufferArg) and
10531040
sizeExprComputableSize(sizeArg, _, sizeArgValue) and
1054-
computedBufferSize = bufferArgSize - sizeMult.(float) * getArithmeticOffsetValue(bufferArg) and
1041+
computedBufferSize = bufferArgSize - sizeMult.(float) * getArithmeticOffsetValue(bufferArg, _) and
10551042
computedSizeAccessed =
10561043
sizeMult.(float) * (sizeArgValue + argNumCharactersOffset(bufferAccess, sizeArg)).(float) and
10571044
computedBufferSize < computedSizeAccessed
@@ -1074,7 +1061,7 @@ module OOB {
10741061
bufferElementSize = fc.getWriteSizeArgMult()
10751062
) and
10761063
bufferUseComputableBufferSize(bufferArg, _, bufferSize) and
1077-
bufferArgOffset = getArithmeticOffsetValue(bufferArg) * bufferElementSize and
1064+
bufferArgOffset = getArithmeticOffsetValue(bufferArg, _) * bufferElementSize and
10781065
bufferArgOffset >= bufferSize
10791066
)
10801067
}
@@ -1100,8 +1087,8 @@ module OOB {
11001087
sourceSizeExpr = source.getSizeExprSource(sourceSizeExprBase, sourceSizeExprOffset) and
11011088
bufferUseNonComputableSize(bufferArg, source) and
11021089
not globalValueNumber(sourceSizeExpr) = globalValueNumber(bufferSizeArg) and
1103-
sizeArgOffset = getArithmeticOffsetValue(bufferSizeArg.getAChild*()) and
1104-
bufferArgOffset = getArithmeticOffsetValue(bufferArg) and
1090+
sizeArgOffset = getArithmeticOffsetValue(bufferSizeArg.getAChild*(), _) and
1091+
bufferArgOffset = getArithmeticOffsetValue(bufferArg, _) and
11051092
sourceSizeExprOffset + bufferArgOffset < sizeArgOffset
11061093
)
11071094
}
@@ -1119,7 +1106,7 @@ module OOB {
11191106
] and
11201107
not fc.getTarget().(BufferAccessLibraryFunction).getAPermissiblyNullParameterIndex(i) and
11211108
bufferArg = fc.getArgument(i) and
1122-
getStatedValue(bufferArg) = 0
1109+
getMinStatedValue(bufferArg) = 0
11231110
)
11241111
}
11251112

@@ -1181,7 +1168,7 @@ module OOB {
11811168
// Not a size expression for which we can compute a specific size
11821169
not sizeExprComputableSize(sizeArg, _, _) and
11831170
// If the lower bound is less than zero, taking into account any offsets
1184-
lowerBound(sizeArg) + getArithmeticOffsetValue(bufferArg) < 0
1171+
lowerBound(sizeArg) + getArithmeticOffsetValue(bufferArg, _) < 0
11851172
)
11861173
}
11871174

0 commit comments

Comments
 (0)