windows-kernel-codeql/KernelSpinlocks.qll at main · gsutherland-trailofbits/windows-kernel-codeql · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
import cpp
import AcquireRelease

class SpinlockAcquire extends AcquireOperation {
    SpinlockAcquire() {
        exists(Function target |
            target = this.getTarget() |
            target.hasGlobalName("KeAcquireSpinLock")
            or target.hasGlobalName("KfAcquireSpinLock") // this is the internal name that the KeAcquireSpinLock macro expands to
            or target.hasGlobalName("KeAcquireSpinLockAtDpcLevel")
            or target.hasGlobalName("KefAcquireSpinLockAtDpcLevel") // this is the internal name that the KeAcquireSpinLockAtDpcLevel macro expands to in some builds
            or target.hasGlobalName("KeAcquireSpinLockForDpc")
            or target.hasGlobalName("KeAcquireSpinLockRaiseToDpc")
            or target.hasGlobalName("KeAcquireInStackQueuedSpinLock")
            or target.hasGlobalName("KeAcquireInStackQueuedSpinLockAtDpcLevel")
            or target.hasGlobalName("KeAcquireInStackQueuedSpinLockForDpc")
        )
    }

    override Variable getAcquired() {
        result.getAnAccess() = this.getArgument(0)
    }

    predicate isMatchingReleaseFunction(Function target) {
        /*
        Many of these can be macros on certain builds so we check the internal function names too.
        */
        (
            (
                this.getTarget().hasGlobalName("KeAcquireSpinLock")
                or this.getTarget().hasGlobalName("KfAcquireSpinLock")
                or this.getTarget().hasGlobalName("KeAcquireSpinLockRaiseToDpc") // this one is released with KeReleaseSpinLock
            )
            and
            (
                target.hasGlobalName("KeReleaseSpinLock")
                or target.hasGlobalName("KfReleaseSpinLock")
            )
        )
        or
        (
            (
                this.getTarget().hasGlobalName("KeAcquireSpinLockAtDpcLevel")
                or this.getTarget().hasGlobalName("KefAcquireSpinLockAtDpcLevel")
            )
            and
            (
                target.hasGlobalName("KeReleaseSpinLockFromDpcLevel")
                or target.hasGlobalName("KefReleaseSpinLockFromDpcLevel")
            )
        )
        or
        (
            this.getTarget().hasGlobalName("KeAcquireSpinLockForDpc")
            and target.hasGlobalName("KeReleaseSpinLockForDpc")
        )
        or
        (
            this.getTarget().hasGlobalName("KeAcquireInStackQueuedSpinLock")
            and target.hasGlobalName("KeReleaseInStackQueuedSpinLock")
        )
        or
        (
            this.getTarget().hasGlobalName("KeAcquireInStackQueuedSpinLockAtDpcLevel")
            and target.hasGlobalName("KeReleaseInStackQueuedSpinLockFromDpcLevel")
        )
        or
        (
            this.getTarget().hasGlobalName("KeAcquireInStackQueuedSpinLockForDpc")
            and target.hasGlobalName("KeReleaseInStackQueuedSpinLockForDpc")
        )
    }

    override ReleaseOperation getMatchingRelease() {
        result.(SpinlockRelease).getReleased() = this.getAcquired()
    }

    override string say() {
        result = "spinlock acquisition of " + this.getAcquired().getName()
    }
}

class SpinlockRelease extends ReleaseOperation {
    SpinlockRelease() {
        exists(Function target |
            target = this.getTarget() |
            target.hasGlobalName("KeReleaseSpinLock")
            or target.hasGlobalName("KfReleaseSpinLock")
            or target.hasGlobalName("KeReleaseSpinLockForDpc")
            or target.hasGlobalName("KeReleaseSpinLockFromDpcLevel")
            or target.hasGlobalName("KefReleaseSpinLockFromDpcLevel")
            or target.hasGlobalName("KeReleaseInStackQueuedSpinLock")
            or target.hasGlobalName("KeReleaseInStackQueuedSpinLockFromDpcLevel")
            or target.hasGlobalName("KeReleaseInStackQueuedSpinLockForDpc")
        )
    }

    Variable getReleased() {
        result.getAnAccess() = this.getArgument(0)
    }

    override AcquireOperation getMatchingAcquire() {
        this = result.(SpinlockAcquire).getMatchingRelease()
    }

    override string say() {
        result = "spinlock release of " + this.getReleased().getName()
    }
}