From 78eec3a3e3ead850e13f3a898924c3110f522aba Mon Sep 17 00:00:00 2001 From: "Jason A. Donenfeld" Date: Mon, 13 Apr 2026 01:01:04 +0200 Subject: [PATCH 1/8] UserModeMemoryReadMultipleTimes: Remove MdlOrigin.originCanWrite The double-fetch query flags pairs of dereferences through memory origins where originCanWrite() is true. MdlOrigin had this set unconditionally, so every pair of accesses through an MDL-mapped pointer was flagged, even pure writes to an output buffer: void *Buf = MmGetSystemAddressForMdlSafe(Mdl, NormalPagePriority); ((MY_IOCTL *)Buf)->Flags = 0; // flagged ((MY_IOCTL *)Buf)->Count = 0; // flagged While usermode does retain write access to MDL-locked pages through its original VA, flagging all of these is not useful in practice, since virtually all direct I/O drivers access the buffer more than once. Signed-off-by: Jason A. Donenfeld --- src/microsoft/code/cpp/public/windows/kernel/MemoryOrigins.qll | 2 -- 1 file changed, 2 deletions(-) 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() } } /** From 7b6ce157c9cb1e9ee5b1ac3fd32adf5510e930f2 Mon Sep 17 00:00:00 2001 From: "Jason A. Donenfeld" Date: Mon, 13 Apr 2026 01:01:13 +0200 Subject: [PATCH 2/8] IllegalFieldAccess2: Follow call chains from DriverEntry The query only allowed MajorFunction access directly inside a DriverEntry function. Drivers that split initialization across helper functions were falsely flagged: VOID InitDispatch(DRIVER_OBJECT *DriverObject) { DriverObject->MajorFunction[IRP_MJ_CREATE] = MyCreate; } NTSTATUS DriverEntry(DRIVER_OBJECT *DriverObject, ...) { InitDispatch(DriverObject); } Follow call chains transitively from DriverEntry so that helpers are recognized. Signed-off-by: Jason A. Donenfeld --- .../IllegalFieldAccess2.ql | 22 ++++++++++++++----- 1 file changed, 17 insertions(+), 5 deletions(-) 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() From f02dad12de4cde79027886280b7082d51cfc9d0e Mon Sep 17 00:00:00 2001 From: "Jason A. Donenfeld" Date: Mon, 13 Apr 2026 01:01:22 +0200 Subject: [PATCH 3/8] Irql: Evaluate _When_ conditions at call sites KeSetEvent is annotated _When_(Wait==1, _IRQL_requires_max_(APC_LEVEL)). When called with Wait=FALSE, the restriction does not apply and DISPATCH_LEVEL is fine. The query unconditionally applied the annotation regardless of argument values: KeAcquireInStackQueuedSpinLock(&Lock, &Handle); // raises to DISPATCH KeSetEvent(&Event, IO_NO_INCREMENT, FALSE); // flagged Evaluate _When_ conditions against compile-time argument values and skip annotations whose conditions are demonstrably false. Signed-off-by: Jason A. Donenfeld --- .../queries/IrqlTooHigh/IrqlTooHigh.ql | 17 ++++++----- .../general/queries/IrqlTooLow/IrqlTooLow.ql | 17 ++++++----- src/drivers/libraries/Irql.qll | 30 +++++++++++++++++++ 3 files changed, 48 insertions(+), 16 deletions(-) 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. */ From 623df00e655aacdd1415b032479d2ddf73c8dbe6 Mon Sep 17 00:00:00 2001 From: "Jason A. Donenfeld" Date: Mon, 13 Apr 2026 01:01:31 +0200 Subject: [PATCH 4/8] IrqlAnnotationIssue: Skip the -1 parse-failure sentinel getIrqlLevel() returns -1 when it cannot parse the annotation, such as _IRQL_saves_ or _When_ conditionals with complex expressions. The query flagged all of these as invalid annotations: _IRQL_saves_ VOID KeAcquireSpinLock(PKSPIN_LOCK Lock, PKIRQL OldIrql); // flagged Filter out the -1 sentinel since these are valid annotations beyond the analyzer's current parsing capability. Signed-off-by: Jason A. Donenfeld --- .../queries/IrqlAnnotationIssue/IrqlAnnotationIssue.ql | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) 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() From 62b6949e2f8d9de553535974880f666385732708 Mon Sep 17 00:00:00 2001 From: "Jason A. Donenfeld" Date: Mon, 13 Apr 2026 01:01:40 +0200 Subject: [PATCH 5/8] InvalidFunctionClassTypedef: Allow _PAGED variants DRIVER_DISPATCH_PAGED is a valid paged variant of DRIVER_DISPATCH for dispatch routines that only run at PASSIVE_LEVEL. The query flagged the mismatch between function class and typedef: _Dispatch_type_(IRP_MJ_DEVICE_CONTROL) static DRIVER_DISPATCH_PAGED MyDispatch; // flagged Recognize _PAGED suffixed typedefs as compatible with their unsuffixed base function class. Signed-off-by: Jason A. Donenfeld --- .../InvalidFunctionClassTypedef.ql | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) 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" From cbf76e2c0a0805f9fa3ac58351c2967398bac1b8 Mon Sep 17 00:00:00 2001 From: "Jason A. Donenfeld" Date: Mon, 13 Apr 2026 01:01:49 +0200 Subject: [PATCH 6/8] OpaqueMdlUse, OpaqueMdlWrite: Exclude local MDL variables Drivers sometimes construct synthetic MDLs on the stack for zero-copy operations. Direct field access is the only way to initialize these: MDL Mdl = { 0 }; Mdl.MappedSystemVa = Buffer; Mdl.ByteCount = Len; Mdl.MdlFlags = MDL_MAPPED_TO_SYSTEM_VA; Exclude accesses on locally-declared MDL struct variables. Accesses through MDL pointers are not excluded, since those typically reference system-provided MDLs. Signed-off-by: Jason A. Donenfeld --- src/drivers/wdm/queries/OpaqueMdlUse/OpaqueMdlUse.ql | 6 +++++- src/drivers/wdm/queries/OpaqueMdlWrite/OpaqueMdlWrite.ql | 6 +++++- 2 files changed, 10 insertions(+), 2 deletions(-) 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 ) } From 6820d66ab65b03160cd03c4a16e78c06a91bcbf7 Mon Sep 17 00:00:00 2001 From: "Jason A. Donenfeld" Date: Mon, 13 Apr 2026 01:03:11 +0200 Subject: [PATCH 7/8] UnguardedNullReturnDereference: Exclude calls to _In_opt_ parameters When a possibly-null return value is passed to a function whose parameter is annotated _In_opt_, the function explicitly handles null. The query was flagging these as unguarded dereferences: OBJ *Obj = LookupObject(...); PutObject(Obj); // flagged, but PutObject takes _In_opt_ OBJ * Exclude calls where the argument's corresponding parameter carries an _opt_ SAL annotation. Signed-off-by: Jason A. Donenfeld --- .../Likely Bugs/UnguardedNullReturnDereference.ql | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/src/microsoft/Likely Bugs/UnguardedNullReturnDereference.ql b/src/microsoft/Likely Bugs/UnguardedNullReturnDereference.ql index 1f3ecacd..e1c54b92 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) { From 05764747d99721b12e3cf04431e3ac38304d2ab2 Mon Sep 17 00:00:00 2001 From: "Jason A. Donenfeld" Date: Mon, 13 Apr 2026 01:04:16 +0200 Subject: [PATCH 8/8] UnguardedNullReturnDereference: Honor _Analysis_assume_ _Analysis_assume_(Expr) tells the analyzer to treat Expr as true. MSVC compiles __assume() into an empty statement with no AST node, but the EmptyStmt remains in the control flow graph at the macro invocation site. The query was not recognizing this as a null guard: NBL *Nbl = DequeueNbl(&Queue); _Analysis_assume_(Nbl); NET_BUFFER_LIST_STATUS(Nbl) = NDIS_STATUS_FAILURE; // flagged Match the EmptyStmt at the _Analysis_assume_ location as a barrier by correlating it with the macro invocation that names the guarded variable. Also match AssumeExpr directly for compilers that emit it. Signed-off-by: Jason A. Donenfeld --- .../Likely Bugs/UnguardedNullReturnDereference.ql | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/src/microsoft/Likely Bugs/UnguardedNullReturnDereference.ql b/src/microsoft/Likely Bugs/UnguardedNullReturnDereference.ql index e1c54b92..b0dc882e 100644 --- a/src/microsoft/Likely Bugs/UnguardedNullReturnDereference.ql +++ b/src/microsoft/Likely Bugs/UnguardedNullReturnDereference.ql @@ -139,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 + ) } }