Reduce false positives compared to SDV for driver tests (#217)

* 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 <Jason@zx2c4.com>

* 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 <Jason@zx2c4.com>

* 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 <Jason@zx2c4.com>

* 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 <Jason@zx2c4.com>

* 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 <Jason@zx2c4.com>

* 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 <Jason@zx2c4.com>

* 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 <Jason@zx2c4.com>

* 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 <Jason@zx2c4.com>

---------

Signed-off-by: Jason A. Donenfeld <Jason@zx2c4.com>
Co-authored-by: NateD-MSFT <34494373+NateD-MSFT@users.noreply.github.com>

Author: zx2c4

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"

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()

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)),

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(),

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. */

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()

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
     )
   }
 

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
     )
   }
 

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
+    )
   }
 }
 

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() }
 }
 
 /**