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
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
//! Checkers for `Alias` and `Owning` properties.
//!
//! `Alias` delegates to [`crate::verify::vm::alias::check_alias_vm`]; `Owning`
//! is a simple liveness check on the target allocation.
use crate::helpers::mir_scan::Checkpoint;
use crate::verify::contract::Property;
use crate::verify::report::CheckResult;
use crate::verify::vm::state::VmState;
use super::PropertyChecker;
impl PropertyChecker {
pub(super) fn check_alias<'z3, 'tcx>(
&self,
vm_state: &VmState<'z3, 'tcx>,
checkpoint: &Checkpoint<'tcx>,
) -> CheckResult {
match crate::verify::vm::alias::check_alias_vm(vm_state, checkpoint) {
crate::verify::vm::alias::VmAliasResult::Proved => CheckResult::ProvedByRule,
crate::verify::vm::alias::VmAliasResult::Failed(_msg) => CheckResult::Failed,
crate::verify::vm::alias::VmAliasResult::Unknown => CheckResult::Unknown,
}
}
pub(super) fn check_owning<'z3, 'tcx>(
&self,
vm_state: &VmState<'z3, 'tcx>,
checkpoint: &Checkpoint<'tcx>,
property: &Property<'tcx>,
) -> CheckResult {
let Some(value) = self.target_value(vm_state, checkpoint, property) else {
return CheckResult::Unknown;
};
let value = self.resolve_pointer_provenance(vm_state, value);
// `p` may be a pointer just derived from an owner (`Box::into_raw` /
// `as_mut_ptr`), whose term still points at the owner's address but whose
// own provenance slot is empty. Fall back to the owner's field provenance.
let alloc_id = value.provenance_alloc_id().or_else(|| {
vm_state
.find_local_by_address(&value.z3_term)
.and_then(|owner| vm_state.owner_ptr_field(owner))
.and_then(|v| v.provenance_alloc_id())
});
let Some(alloc_id) = alloc_id else {
return CheckResult::ProvedByRule;
};
// `Owning(container.iter())` for_each: every element pointer is the
// sole owner of its pointee, so a pointer loaded from the container
// (whose provenance names the container allocation) is a valid owner.
if vm_state.alloc(alloc_id).facts.for_each.owning {
return CheckResult::ProvedByRule;
}
// A loop-unrolled path repeats the same block (the SCC body), so its
// second `DropMemory` is an unrolled iteration rather than a genuine
// same-iteration double free. Only the non-unrolled path distinguishes
// them (uaf_10 drops twice in one iteration; uaf_false_2 drops once).
if vm_state.path_facts.reenter {
return CheckResult::ProvedByRule;
}
// Owning(p): p is the sole carrier of *p's ownership. A live `needs_drop`
// owner whose buffer aliases `alloc_id` means a second owner will drop the
// same allocation — a double free. The reconstructed owner (the call's
// destination) is not a violation, so exclude it.
let dest_local = checkpoint.destination.or_else(|| {
let body = vm_state.tcx.optimized_mir(checkpoint.caller);
match &body.basic_blocks[checkpoint.block].terminator().kind {
rustc_middle::mir::TerminatorKind::Call { destination, .. } => {
Some(destination.local)
}
_ => None,
}
});
// The local the `Owning(p)` argument names (e.g. `raw` in
// `Box::from_raw(raw)`), resolved to the caller's local.
let raw_local = property.target_place().and_then(|cp| match cp.base {
crate::verify::contract::PlaceBase::Arg(n) => checkpoint
.args
.get(n)
.and_then(|op| crate::helpers::mir_utils::operand_mir_place(op).map(|p| p.local)),
crate::verify::contract::PlaceBase::Local(n) => {
Some(rustc_middle::mir::Local::from_usize(n))
}
crate::verify::contract::PlaceBase::Return => None,
});
let live = crate::verify::vm::alias_hazard::live_locals_at(
vm_state.tcx,
checkpoint.caller,
checkpoint.block,
// `Owning` fires at a call terminator; scan the whole block so a
// `StorageDead` of a consumed parameter (`Box::into_raw(value)`) in
// the same block still counts as dead.
usize::MAX,
true,
true,
);
let typing_env =
rustc_middle::ty::TypingEnv::non_body_analysis(vm_state.tcx, checkpoint.caller);
// `p`'s term often points at the owner's address (e.g. `s.as_mut_ptr()`
// yields a term `addr__1` for `s`). Trace it back to the owner local and
// report a second owner directly, without needing its field provenance.
// A moved-out source still has the same term but its owner-field
// provenance has been invalidated, so it is not counted as an owner.
if let Some(owner) = vm_state.find_local_by_address(&value.z3_term) {
if live.contains(&owner)
&& Some(owner) != dest_local
&& Some(owner) != raw_local
&& vm_state
.owner_ptr_field(owner)
.is_some_and(|f| f.provenance_alloc_id() == Some(alloc_id))
{
let oty = vm_state.body().local_decls[owner].ty;
if oty.needs_drop(vm_state.tcx, typing_env) {
return CheckResult::Failed;
}
}
}
for local in vm_state.current_frame.local_alloc.keys() {
if Some(*local) == dest_local {
continue;
}
if !live.contains(local) {
continue;
}
let ty = vm_state.body().local_decls[*local].ty;
if !ty.needs_drop(vm_state.tcx, typing_env) {
continue;
}
for path in vm_state.field_paths(*local) {
let Some(val) = vm_state.field_value(*local, &path) else {
continue;
};
if val.provenance_alloc_id() != Some(alloc_id) {
continue;
}
return CheckResult::Failed;
}
}
CheckResult::ProvedByRule
}
}