diff --git a/src/drivers/general/queries/FloatSafeExit/FloatSafeExit.qhelp b/src/drivers/general/queries/FloatSafeExit/FloatSafeExit.qhelp new file mode 100644 index 00000000..ed561fca --- /dev/null +++ b/src/drivers/general/queries/FloatSafeExit/FloatSafeExit.qhelp @@ -0,0 +1,69 @@ + + + +

+ Exiting while holding the right to use floating-point hardware +

+
+ +

+ The _Kernel_float_restored_ annotation was used to release the right to use floating point, but a path through the function was detected where no function known to perform that operation was successfully called. This warning might indicate that a conditional (_When_) annotation is needed, or it might indicate a coding error. +

+
+ +

+ Example of function with multiple issues +

+ + +
+ +

+

+
+ +
  • + + Warning C28162 + +
  • +
    +
    diff --git a/src/drivers/general/queries/FloatSafeExit/FloatSafeExit.ql b/src/drivers/general/queries/FloatSafeExit/FloatSafeExit.ql new file mode 100644 index 00000000..5290edc1 --- /dev/null +++ b/src/drivers/general/queries/FloatSafeExit/FloatSafeExit.ql @@ -0,0 +1,108 @@ +// Copyright (c) Microsoft Corporation. +// Licensed under the MIT license. +/** + * @id cpp/drivers/kmdf/float-safe-exit + * @kind problem + * @name Float Safe Exit + * @description Exiting while holding the right to use floating-point hardware + * @platform Desktop + * @feature.area Multiple + * @impact Insecure Coding Practice + * @repro.text + * @owner.email: sdat@microsoft.com + * @opaqueid CQLD-C28162 + * @problem.severity warning + * @precision medium + * @tags correctness + * @scope domainspecific + * @query-version v1 + */ + +import cpp +import semmle.code.cpp.dataflow.new.DataFlow +import drivers.libraries.SAL +import drivers.kmdf.libraries.KmdfDrivers +import semmle.code.cpp.Specifier + +class KernelFloatFunctionAnnotation extends SALAnnotation { + KernelFloatFunctionAnnotation() { this.getMacroName().matches(["_Kernel_float_restored_"]) } +} + +class KernelFloatAnnotatedTypedef extends TypedefType { + KernelFloatFunctionAnnotation kernelFloatAnnotation; + + KernelFloatAnnotatedTypedef() { kernelFloatAnnotation.getTypedefDeclarations() = this } + + KernelFloatFunctionAnnotation getKernelFloatAnnotation() { result = kernelFloatAnnotation } +} + +class KernelFloatAnnotatedFunction extends Function { + KernelFloatFunctionAnnotation kernelFloatAnnotation; + + cached + KernelFloatAnnotatedFunction() { + ( + // this.hasCLinkage() and + exists( + FunctionDeclarationEntry fde // actual function declarations + | + fde = this.getADeclarationEntry() and + kernelFloatAnnotation.getDeclarationEntry() = fde + ) + or + exists( + FunctionDeclarationEntry fde // typedefs + | + fde.getFunction() = this and + fde.getTypedefType().(KernelFloatAnnotatedTypedef).getKernelFloatAnnotation() = + kernelFloatAnnotation + ) + ) + } +} + +class SafeFloatRestoreFuncCall extends FunctionCall { + SafeFloatRestoreFuncCall() { + this.getTarget().getName() = ("KeRestoreFloatingPointState") or + this.getTarget().getName() = ("EngRestoreFloatingPointState") + } +} + +class SafeFloatRestoreFunc extends Function { + SafeFloatRestoreFunc() { + this.getName() = ("KeRestoreFloatingPointState") or + this.getName() = ("EngRestoreFloatingPointState") + } +} + +predicate unused(Expr e) { e instanceof ExprInVoidContext } + +from FunctionCall unusedFc, KernelFloatAnnotatedFunction kernelFloatFunc, BasicBlock bb, string msg +where + ( + // each path must have a call to a float save function + bb.getEnclosingFunction() = kernelFloatFunc and + not exists(SafeFloatRestoreFuncCall safeFloatRestoreFuncCall, ControlFlowNode node | + bb.getNode(0).getASuccessor*().getBasicBlock().contains(node) and + node = safeFloatRestoreFuncCall.getBasicBlock().getANode() and + safeFloatRestoreFuncCall.getEnclosingFunction() = kernelFloatFunc + ) and + msg = + "Function annotated with _Kernel_float_restored_ but does not call a safe float access function for some path(s)" + or + // Paths have call to safe float access function but return value is not used + unusedFc instanceof SafeFloatRestoreFuncCall and + unusedFc.getEnclosingFunction() = kernelFloatFunc and + msg = + "Function annotated with _Kernel_float_restored_ but does not check a safe float access function return value for some path(s)" and + ( + // return value isn't used at all + unused(unusedFc) + or + // return value saved to variable but not used + definition(_, unusedFc.getParent()) and + not definitionUsePair(_, unusedFc.getParent(), _) + ) + ) and + not kernelFloatFunc instanceof SafeFloatRestoreFunc +select kernelFloatFunc, msg diff --git a/src/drivers/general/queries/FloatSafeExit/FloatSafeExit.sarif b/src/drivers/general/queries/FloatSafeExit/FloatSafeExit.sarif new file mode 100644 index 00000000..0f245a3a --- /dev/null +++ b/src/drivers/general/queries/FloatSafeExit/FloatSafeExit.sarif @@ -0,0 +1,367 @@ +{ + "$schema": "https://json.schemastore.org/sarif-2.1.0.json", + "version": "2.1.0", + "runs": [ + { + "tool": { + "driver": { + "name": "CodeQL", + "organization": "GitHub", + "semanticVersion": "2.17.6", + "notifications": [ + { + "id": "cpp/baseline/expected-extracted-files", + "name": "cpp/baseline/expected-extracted-files", + "shortDescription": { + "text": "Expected extracted files" + }, + "fullDescription": { + "text": "Files appearing in the source archive that are expected to be extracted." + }, + "defaultConfiguration": { + "enabled": true + }, + "properties": { + "tags": [ + "expected-extracted-files", + "telemetry" + ] + } + }, + { + "id": "cpp/extractor/summary", + "name": "cpp/extractor/summary", + "shortDescription": { + "text": "C++ extractor telemetry" + }, + "fullDescription": { + "text": "C++ extractor telemetry" + }, + "defaultConfiguration": { + "enabled": true + } + } + ], + "rules": [ + { + "id": "cpp/drivers/kmdf/float-safe-exit", + "name": "cpp/drivers/kmdf/float-safe-exit", + "shortDescription": { + "text": "Float Safe Exit" + }, + "fullDescription": { + "text": "Exiting while holding the right to use floating-point hardware" + }, + "defaultConfiguration": { + "enabled": true, + "level": "warning" + }, + "properties": { + "tags": [ + "correctness" + ], + "description": "Exiting while holding the right to use floating-point hardware", + "feature.area": "Multiple", + "id": "cpp/drivers/kmdf/float-safe-exit", + "impact": "Insecure Coding Practice", + "kind": "problem", + "name": "Float Safe Exit", + "opaqueid": "CQLD-C28162", + "owner.email:": "sdat@microsoft.com", + "platform": "Desktop", + "precision": "medium", + "problem.severity": "warning", + "query-version": "v1", + "repro.text": "", + "scope": "domainspecific" + } + } + ] + }, + "extensions": [ + { + "name": "microsoft/windows-drivers", + "semanticVersion": "1.1.0+ce7d70c32c8e0908d7c329389aa84ac3a89e7feb", + "locations": [ + { + "uri": "file:///C:/codeql-home/WDDST/src/", + "description": { + "text": "The QL pack root directory." + } + }, + { + "uri": "file:///C:/codeql-home/WDDST/src/qlpack.yml", + "description": { + "text": "The QL pack definition file." + } + } + ] + } + ] + }, + "invocations": [ + { + "toolExecutionNotifications": [ + { + "locations": [ + { + "physicalLocation": { + "artifactLocation": { + "uri": "driver/driver_snippet.c", + "uriBaseId": "%SRCROOT%", + "index": 0 + } + } + } + ], + "message": { + "text": "" + }, + "level": "none", + "descriptor": { + "id": "cpp/baseline/expected-extracted-files", + "index": 0 + }, + "properties": { + "formattedMessage": { + "text": "" + } + } + }, + { + "locations": [ + { + "physicalLocation": { + "artifactLocation": { + "uri": "driver/fail_driver1.h", + "uriBaseId": "%SRCROOT%", + "index": 1 + } + } + } + ], + "message": { + "text": "" + }, + "level": "none", + "descriptor": { + "id": "cpp/baseline/expected-extracted-files", + "index": 0 + }, + "properties": { + "formattedMessage": { + "text": "" + } + } + }, + { + "locations": [ + { + "physicalLocation": { + "artifactLocation": { + "uri": "driver/fail_driver1.c", + "uriBaseId": "%SRCROOT%", + "index": 2 + } + } + } + ], + "message": { + "text": "" + }, + "level": "none", + "descriptor": { + "id": "cpp/baseline/expected-extracted-files", + "index": 0 + }, + "properties": { + "formattedMessage": { + "text": "" + } + } + }, + { + "message": { + "text": "Internal telemetry for the C++ extractor.\n\nNo action needed.", + "markdown": "Internal telemetry for the C++ extractor.\n\nNo action needed." + }, + "level": "note", + "timeUtc": "2024-08-21T03:59:26.732+00:00", + "descriptor": { + "id": "cpp/extractor/summary", + "index": 1 + }, + "properties": { + "attributes": { + "cache-hits": 0, + "cache-misses": 1, + "extractor-failures": 1, + "extractor-successes": 0, + "trap-caching": "disabled" + }, + "visibility": { + "statusPage": false, + "telemetry": true + } + } + } + ], + "executionSuccessful": true + } + ], + "artifacts": [ + { + "location": { + "uri": "driver/driver_snippet.c", + "uriBaseId": "%SRCROOT%", + "index": 0 + } + }, + { + "location": { + "uri": "driver/fail_driver1.h", + "uriBaseId": "%SRCROOT%", + "index": 1 + } + }, + { + "location": { + "uri": "driver/fail_driver1.c", + "uriBaseId": "%SRCROOT%", + "index": 2 + } + } + ], + "results": [ + { + "ruleId": "cpp/drivers/kmdf/float-safe-exit", + "ruleIndex": 0, + "rule": { + "id": "cpp/drivers/kmdf/float-safe-exit", + "index": 0 + }, + "message": { + "text": "Function annotated with _Kernel_float_restored_ but does not check a safe float access function return value for some path(s)\nFunction annotated with _Kernel_float_restored_ but does not call a safe float access function for some path(s)" + }, + "locations": [ + { + "physicalLocation": { + "artifactLocation": { + "uri": "driver/driver_snippet.c", + "uriBaseId": "%SRCROOT%", + "index": 0 + }, + "region": { + "startLine": 69, + "startColumn": 30, + "endColumn": 45 + } + } + } + ], + "partialFingerprints": { + "primaryLocationLineHash": "386e94a812f5ee7b:1", + "primaryLocationStartColumnFingerprint": "29" + } + }, + { + "ruleId": "cpp/drivers/kmdf/float-safe-exit", + "ruleIndex": 0, + "rule": { + "id": "cpp/drivers/kmdf/float-safe-exit", + "index": 0 + }, + "message": { + "text": "Function annotated with _Kernel_float_restored_ but does not call a safe float access function for some path(s)" + }, + "locations": [ + { + "physicalLocation": { + "artifactLocation": { + "uri": "driver/driver_snippet.c", + "uriBaseId": "%SRCROOT%", + "index": 0 + }, + "region": { + "startLine": 60, + "startColumn": 30, + "endColumn": 45 + } + } + } + ], + "partialFingerprints": { + "primaryLocationLineHash": "6c5b6cd6863fe3a0:1", + "primaryLocationStartColumnFingerprint": "29" + } + }, + { + "ruleId": "cpp/drivers/kmdf/float-safe-exit", + "ruleIndex": 0, + "rule": { + "id": "cpp/drivers/kmdf/float-safe-exit", + "index": 0 + }, + "message": { + "text": "Function annotated with _Kernel_float_restored_ but does not check a safe float access function return value for some path(s)\nFunction annotated with _Kernel_float_restored_ but does not call a safe float access function for some path(s)" + }, + "locations": [ + { + "physicalLocation": { + "artifactLocation": { + "uri": "driver/driver_snippet.c", + "uriBaseId": "%SRCROOT%", + "index": 0 + }, + "region": { + "startLine": 43, + "startColumn": 30, + "endColumn": 45 + } + } + } + ], + "partialFingerprints": { + "primaryLocationLineHash": "8df2b9dba2f4259a:1", + "primaryLocationStartColumnFingerprint": "29" + } + }, + { + "ruleId": "cpp/drivers/kmdf/float-safe-exit", + "ruleIndex": 0, + "rule": { + "id": "cpp/drivers/kmdf/float-safe-exit", + "index": 0 + }, + "message": { + "text": "Function annotated with _Kernel_float_restored_ but does not check a safe float access function return value for some path(s)\nFunction annotated with _Kernel_float_restored_ but does not call a safe float access function for some path(s)" + }, + "locations": [ + { + "physicalLocation": { + "artifactLocation": { + "uri": "driver/driver_snippet.c", + "uriBaseId": "%SRCROOT%", + "index": 0 + }, + "region": { + "startLine": 19, + "startColumn": 30, + "endColumn": 46 + } + } + } + ], + "partialFingerprints": { + "primaryLocationLineHash": "e257ac675879444e:1", + "primaryLocationStartColumnFingerprint": "29" + } + } + ], + "columnKind": "utf16CodeUnits", + "properties": { + "semmle.formatSpecifier": "sarifv2.1.0" + } + } + ] +} \ No newline at end of file diff --git a/src/drivers/general/queries/FloatSafeExit/driver_snippet.c b/src/drivers/general/queries/FloatSafeExit/driver_snippet.c new file mode 100644 index 00000000..86104687 --- /dev/null +++ b/src/drivers/general/queries/FloatSafeExit/driver_snippet.c @@ -0,0 +1,104 @@ +// Copyright (c) Microsoft Corporation. +// Licensed under the MIT license. + +// Macros to enable or disable a code section that may or may not conflict with this test. +#define SET_DISPATCH 1 +int _fltused; + +// Template function. Not used for this test. +void top_level_call() +{ +} + +void float_used_good0() +{ + float f = 0.0f; + f = f + 1.0f; +} + +_Kernel_float_restored_ void float_used_good1() +{ + KFLOATING_SAVE saveData; + NTSTATUS status; + float f = 0.0f; + status = KeSaveFloatingPointState(&saveData); + if (status != STATUS_SUCCESS) + { + status = KeRestoreFloatingPointState(&saveData); + return; + } + for (int i = 0; i < 100; i++) + { + f = f + 1.0f; + } + status = KeRestoreFloatingPointState(&saveData); + if (!NT_SUCCESS(status)) + { + ; + // handle error + } +} + +// Fail cases +_Kernel_float_restored_ void float_used_bad1() +{ + KFLOATING_SAVE saveData; + NTSTATUS status; + float f = 0.0f; + status = KeSaveFloatingPointState(&saveData); + if (!NT_SUCCESS(status)) + { + return; + } + for (int i = 0; i < 100; i++) + { + f = f + 1.0f; + } + // doesn't check the return value of KeRestoreFloatingPointState + KeRestoreFloatingPointState(&saveData); +} +_Kernel_float_restored_ void float_used_bad2() +{ + float f = 0.0f; + for (int i = 0; i < 100; i++) + { + f = f + 1.0f; + } + // No call to KeRestoreFloatingPointState +} +_Kernel_float_restored_ void float_used_bad3() +{ + float f = 0.0f; + int some_condition = 1; + KFLOATING_SAVE saveData; + NTSTATUS status; + + if (some_condition) + { + status = KeSaveFloatingPointState(&saveData); + if (!NT_SUCCESS(status)) + { + return; + } + for (int i = 0; i < 100; i++) + { + f = f + 1; + } + // doesn't restore the floating point state + } + else + { + status = KeSaveFloatingPointState(&saveData); + if (!NT_SUCCESS(status)) + { + return; + } + for (int i = 0; i < 100; i++) + { + f = f + 1.0f; + } + + // doesn't check the return value of KeRestoreFloatingPointState + status = KeRestoreFloatingPointState(&saveData); + } +} diff --git a/src/drivers/test/diff/FloatSafeExit.sarif b/src/drivers/test/diff/FloatSafeExit.sarif new file mode 100644 index 00000000..dea8275e --- /dev/null +++ b/src/drivers/test/diff/FloatSafeExit.sarif @@ -0,0 +1,21 @@ +{ + "all": { + "+": 0, + "-": 0 + }, + "error": { + "+": 0, + "-": 0, + "codes": [] + }, + "warning": { + "+": 0, + "-": 0, + "codes": [] + }, + "note": { + "+": 0, + "-": 0, + "codes": [] + } +} \ No newline at end of file