diff --git a/src/drivers/general/queries/InvalidFunctionClassTypedef/InvalidFunctionClassTypedef.ql b/src/drivers/general/queries/InvalidFunctionClassTypedef/InvalidFunctionClassTypedef.ql index a93e6462..275e52f2 100644 --- a/src/drivers/general/queries/InvalidFunctionClassTypedef/InvalidFunctionClassTypedef.ql +++ b/src/drivers/general/queries/InvalidFunctionClassTypedef/InvalidFunctionClassTypedef.ql @@ -16,7 +16,7 @@ * @tags correctness * ca_ported * @scope domainspecific - * @query-version v1 + * @query-version v2 */ import cpp @@ -73,6 +73,11 @@ where not ( funcClass.matches("EVT_WDF_DEVICE_%ARM_WAKE_FROM_S%") and declTypedef.matches("EVT_WDF_DEVICE_%ARM_WAKE_FROM_S%") + ) and + not ( + declTypedef = funcClass + "_PAGED" + or + funcClass = declTypedef + "_PAGED" ) select af, "The function class " + funcClass + " on the function does not match the function class " + declTypedef + " on the typedef used here" diff --git a/src/drivers/general/queries/IrqlAnnotationIssue/IrqlAnnotationIssue.ql b/src/drivers/general/queries/IrqlAnnotationIssue/IrqlAnnotationIssue.ql index d7e4c8cd..d9fe3bdb 100644 --- a/src/drivers/general/queries/IrqlAnnotationIssue/IrqlAnnotationIssue.ql +++ b/src/drivers/general/queries/IrqlAnnotationIssue/IrqlAnnotationIssue.ql @@ -18,12 +18,14 @@ * @tags correctness * ca_ported * @scope domainspecific - * @query-version v1 + * @query-version v2 */ import cpp import drivers.libraries.Irql from IrqlFunctionAnnotation ifa -where not ifa.getIrqlLevel() instanceof IrqlValue +where + not ifa.getIrqlLevel() instanceof IrqlValue and + ifa.getIrqlLevel() != -1 select ifa, "Invalid IRQL annotation: " + ifa.getIrqlLevel() diff --git a/src/drivers/general/queries/IrqlTooHigh/IrqlTooHigh.ql b/src/drivers/general/queries/IrqlTooHigh/IrqlTooHigh.ql index c678aa66..b49a762e 100644 --- a/src/drivers/general/queries/IrqlTooHigh/IrqlTooHigh.ql +++ b/src/drivers/general/queries/IrqlTooHigh/IrqlTooHigh.ql @@ -18,23 +18,24 @@ * ca_ported * wddst * @scope domainspecific - * @query-version v2 + * @query-version v3 */ import cpp import drivers.libraries.Irql -from FunctionCall call, IrqlRestrictsFunction irqlFunc, ControlFlowNode prior, int irqlRequirement +from + FunctionCall call, IrqlRestrictsFunction irqlFunc, ControlFlowNode prior, int irqlRequirement, + IrqlFunctionAnnotation ifa where call.getTarget() = irqlFunc and prior = call.getAPredecessor() and - ( - irqlFunc.(IrqlMaxAnnotatedFunction).getIrqlLevel() = irqlRequirement - or - irqlFunc.(IrqlRequiresAnnotatedFunction).getIrqlLevel() = irqlRequirement - ) and + ifa = irqlFunc.getFuncIrqlAnnotation() and + (ifa instanceof IrqlMaxAnnotation or ifa instanceof IrqlRequiresAnnotation) and + irqlRequirement = ifa.getIrqlLevel() and irqlRequirement != -1 and - irqlRequirement < min(getPotentialExitIrqlAtCfn(prior)) + irqlRequirement < min(getPotentialExitIrqlAtCfn(prior)) and + not ifa.whenConditionIsFalseAtCallSite(call) select call, "$@: IRQL potentially too high at call to $@. Maximum IRQL for this call: " + irqlRequirement + ", IRQL at preceding node: " + min(getPotentialExitIrqlAtCfn(prior)), diff --git a/src/drivers/general/queries/IrqlTooLow/IrqlTooLow.ql b/src/drivers/general/queries/IrqlTooLow/IrqlTooLow.ql index 9a016373..e85c72a6 100644 --- a/src/drivers/general/queries/IrqlTooLow/IrqlTooLow.ql +++ b/src/drivers/general/queries/IrqlTooLow/IrqlTooLow.ql @@ -18,23 +18,24 @@ * ca_ported * wddst * @scope domainspecific - * @query-version v3 + * @query-version v4 */ import cpp import drivers.libraries.Irql -from FunctionCall call, IrqlRestrictsFunction irqlFunc, ControlFlowNode prior, int irqlRequirement +from + FunctionCall call, IrqlRestrictsFunction irqlFunc, ControlFlowNode prior, int irqlRequirement, + IrqlFunctionAnnotation ifa where call.getTarget() = irqlFunc and prior = call.getAPredecessor() and - ( - irqlFunc.(IrqlMinAnnotatedFunction).getIrqlLevel() = irqlRequirement - or - irqlFunc.(IrqlRequiresAnnotatedFunction).getIrqlLevel() = irqlRequirement - ) and + ifa = irqlFunc.getFuncIrqlAnnotation() and + (ifa instanceof IrqlMinAnnotation or ifa instanceof IrqlRequiresAnnotation) and + irqlRequirement = ifa.getIrqlLevel() and irqlRequirement != -1 and - irqlRequirement > max(getPotentialExitIrqlAtCfn(prior)) + irqlRequirement > max(getPotentialExitIrqlAtCfn(prior)) and + not ifa.whenConditionIsFalseAtCallSite(call) select call, "$@: IRQL potentially too low at call to $@. Minimum IRQL for this call: " + irqlRequirement + ", IRQL at preceding node: " + max(getPotentialExitIrqlAtCfn(prior)), call.getControlFlowScope(), diff --git a/src/drivers/libraries/Irql.qll b/src/drivers/libraries/Irql.qll index 19907787..cb01e1be 100644 --- a/src/drivers/libraries/Irql.qll +++ b/src/drivers/libraries/Irql.qll @@ -208,6 +208,36 @@ then result = this.getIrqlLevelString().toInt() else result = -1 } + + /** + * Holds if this is a `_When_` annotation whose condition is demonstrably + * false at call site `call`. + * + * Callers should only pass the annotation that supplied the IRQL + * requirement being checked -- otherwise an unrelated `_When_` clause on + * the same function (e.g. the `Wait==1` clause when we are evaluating the + * `Wait==0` clause on `KeSetEvent`) would suppress legitimate findings. + */ + predicate whenConditionIsFalseAtCallSite(FunctionCall call) { + this.getMacroName() = "_When_" and + exists(string cond, string paramName, int paramIdx | + cond = this.getUnexpandedArgument(0) and + call.getTarget().getParameter(paramIdx).getName() = paramName and + ( + // "Param != 0" is false when arg is 0 + paramName = cond.regexpCapture("(\\w+)\\s*!=\\s*0", 1) and + call.getArgument(paramIdx).getValue() = "0" + or + // "Param == N" (N>0) is false when arg is 0 + paramName = cond.regexpCapture("(\\w+)\\s*==\\s*([1-9]\\d*)", 1) and + call.getArgument(paramIdx).getValue() = "0" + or + // "Param == 0" is false when arg is nonzero + paramName = cond.regexpCapture("(\\w+)\\s*==\\s*0", 1) and + call.getArgument(paramIdx).getValue() != "0" + ) + ) + } } /** Represents an "\_IRQL\_requires\_same\_" annotation. */ diff --git a/src/drivers/wdm/queries/IllegalFieldAccess2/IllegalFieldAccess2.ql b/src/drivers/wdm/queries/IllegalFieldAccess2/IllegalFieldAccess2.ql index 94747c89..ed72d22f 100644 --- a/src/drivers/wdm/queries/IllegalFieldAccess2/IllegalFieldAccess2.ql +++ b/src/drivers/wdm/queries/IllegalFieldAccess2/IllegalFieldAccess2.ql @@ -18,7 +18,7 @@ * ca_ported * wddst * @scope domainspecific - * @query-version v1 + * @query-version v2 */ import cpp @@ -87,6 +87,19 @@ class IllegalDeviceObjectFieldAccess extends FieldAccess, PotentiallyIllegalFiel } } +/** + * Holds if `f` is `DriverEntry` itself or is transitively called from + * `DriverEntry`. + */ +predicate calledFromDriverEntry(Function f) { + f instanceof WdmDriverEntry + or + exists(Function caller | + calledFromDriverEntry(caller) and + f.getACallToThisFunction().getEnclosingFunction() = caller + ) +} + /** * A potentially illegal access to a DriverObject field, namely: * - Accesses to a DriverObject's DriverStartIo, DriverUnload, MajorFunction, and DriverExtension fields outside DriverEntry @@ -119,15 +132,14 @@ class IllegalDriverObjectFieldAccess extends FieldAccess, PotentiallyIllegalFiel override predicate isIllegalAccess() { /* - * Below fields are illegal iff we're not in a DriverEntry function. - * Possible future improvement: do flow analysis to figure out if we're in - * a call from a DriverEntry routine. + * Below fields are illegal iff we're not in a DriverEntry function or a + * function transitively called from DriverEntry. */ this.getTarget() .getName() .matches(["DriverStartIo", "DriverUnload", "MajorFunction", "DriverExtension"]) and - not this.getControlFlowScope() instanceof WdmDriverEntry + not calledFromDriverEntry(this.getControlFlowScope()) or not this.getTarget() .getName() diff --git a/src/drivers/wdm/queries/OpaqueMdlUse/OpaqueMdlUse.ql b/src/drivers/wdm/queries/OpaqueMdlUse/OpaqueMdlUse.ql index 87a08dcc..970eb9ec 100644 --- a/src/drivers/wdm/queries/OpaqueMdlUse/OpaqueMdlUse.ql +++ b/src/drivers/wdm/queries/OpaqueMdlUse/OpaqueMdlUse.ql @@ -17,7 +17,7 @@ * @tags correctness * wddst * @scope domainspecific - * @query-version v1 + * @query-version v2 */ import cpp @@ -42,6 +42,10 @@ class IncorrectMdlFieldAccess extends FieldAccess { exists(SafeMdlAccessMacro safeMacro | safeMacro.getAnInvocation().getAnExpandedElement() = this ) + ) and + not exists(LocalVariable lv | + lv.getType().getUnspecifiedType() instanceof Mdl and + this.getQualifier().(VariableAccess).getTarget() = lv ) } diff --git a/src/drivers/wdm/queries/OpaqueMdlWrite/OpaqueMdlWrite.ql b/src/drivers/wdm/queries/OpaqueMdlWrite/OpaqueMdlWrite.ql index 9eb37aa9..bebf0041 100644 --- a/src/drivers/wdm/queries/OpaqueMdlWrite/OpaqueMdlWrite.ql +++ b/src/drivers/wdm/queries/OpaqueMdlWrite/OpaqueMdlWrite.ql @@ -18,7 +18,7 @@ * ca_ported * wddst * @scope domainspecific - * @query-version v1 + * @query-version v2 */ import cpp @@ -43,6 +43,10 @@ class IncorrectMdlWrite extends Assignment { exists(SafeMdlWriteMacro safeWriteMacro | safeWriteMacro.getAnInvocation().getAnExpandedElement() = this ) + ) and + not exists(LocalVariable lv | + lv.getType().getUnspecifiedType() instanceof Mdl and + access.getQualifier().(VariableAccess).getTarget() = lv ) } diff --git a/src/microsoft/Likely Bugs/UnguardedNullReturnDereference.ql b/src/microsoft/Likely Bugs/UnguardedNullReturnDereference.ql index 1f3ecacd..b0dc882e 100644 --- a/src/microsoft/Likely Bugs/UnguardedNullReturnDereference.ql +++ b/src/microsoft/Likely Bugs/UnguardedNullReturnDereference.ql @@ -79,7 +79,14 @@ class UnguardedNullReturnDereferenceReachability extends StackVariableReachabili .getDereferencingOperation() .(FunctionCall) .getTarget() - .hasGlobalName("free") + .hasGlobalName("free") and + not exists(FunctionCall fc, int i | + fc = node.(Dereference).getDereferencingOperation() and + fc.getArgument(i) = v.getAnAccess() and + exists(SALMaybeNull sa | + sa.getDeclaration() = fc.getTarget().getParameter(i) + ) + ) } override predicate isBarrier(ControlFlowNode node, StackVariable v) { @@ -132,6 +139,19 @@ class UnguardedNullReturnDereferenceReachability extends StackVariableReachabili "_checked_pointer_impl", "_fail_on_unexpected_null_pointer", "_fail_on_memory_op"] and c.getAnArgument().getAChild*() = v.getAnAccess() and c = node) + or + exists(AssumeExpr ae | + ae = node and + ae.getOperand().getAChild*() = v.getAnAccess() + ) + or + exists(MacroInvocation mi | + mi.getMacroName() = "_Analysis_assume_" and + mi.getUnexpandedArgument(0) = v.getName() and + node.getLocation().getFile() = mi.getLocation().getFile() and + node.getLocation().getStartLine() = mi.getLocation().getStartLine() and + node instanceof EmptyStmt + ) } } diff --git a/src/microsoft/code/cpp/public/windows/kernel/MemoryOrigins.qll b/src/microsoft/code/cpp/public/windows/kernel/MemoryOrigins.qll index e34a65ee..620c1d36 100644 --- a/src/microsoft/code/cpp/public/windows/kernel/MemoryOrigins.qll +++ b/src/microsoft/code/cpp/public/windows/kernel/MemoryOrigins.qll @@ -177,8 +177,6 @@ class MdlOrigin extends DirectMemoryOrigin, FunctionCall { } override Expr getABufferSizeExpression() { none() } - - override predicate originCanWrite() { any() } } /**