notesum.ai

Published at December 9

Fearless unsafe. Safety Property is all you need

cs.SE

Released Date: December 9, 2024

Authors: Mohan Cui¹, Penglei Mao¹, Shuran Sun¹, Yangfan Zhou¹, Hui Xu¹

Aff.: ¹Fudan University

Arxiv: http://arxiv.org/pdf/2412.06251v1

Safety Property	SUM	Definition and the safety requirement of each Safety Property.	Unsafe API Example
Precondition Safety Property
Allocated $\blacktriangle$	172	Non-Null $\blacktriangle$ : A null pointer is never valid, not even for accesses of size zero.	impl¡T: Sized¿ NonNull¡T¿::new_unchecked
Allocated $\blacktriangle$	172	Non-Dangling $\blacktriangledown$ : The value must not be pointing to the deallocated memory even for operations of size zero, including data stored in the stack frame and heap chunk.	trait SliceIndex¡T: ?Sized¿::get_unchecked
Bounded $\blacktriangledown$	141	Numerical: The relationship expressions based on numerical operations exhibit clear numerical boundaries. The terms of the expressions can be constants, variables, or the return values of function calls. There are six relational operators including EQ, NE, LT, GT, LE, and GE.	impl¡T: ?Sized¿ *mut T::offset_from
Bounded $\blacktriangledown$	141	Dereferencable: The memory range of the given size starting at the pointer must all be within the bounds of a single allocated object.	impl¡T: ?Sized¿ *mut T::copy_from
Initialized $\blacktriangledown$	104	Initialized $\blacktriangle$ : The value that has been initialized can be divided into two scenarios: fully initialized and partially initialized.	impl¡T¿ MaybeUninit¡T¿::assume_init
		Typed $\blacktriangledown$ : The bit pattern of the initialized value must be valid at the given type and uphold additional invariants for generics.	impl¡T: ?Sized¿ *mut T::read
		Encoded $\blacktriangledown$ : The encoding format of the string includes UTF-8 string, ASCII string (in bytes), and C-compatible string (nul-terminated trailing with no nul bytes in the middle).	impl String::from_utf8_unchecked
Layout $\blacktriangledown$	109	Sized $\blacktriangle$ : The restrictions on Exotically Sized Types (EST), including Dynamically Sized Types (DST) that lack a statically known size, such as trait objects and slices; and Zero Sized Types (ZST) that occupy no space.	core::mem::size_of_raw
		Aligned $\blacktriangle$ : The value is properly aligned via a specific allocator or the attribute #[repr], including the alignment and the padding.	impl¡T: ?Sized¿ *mut T::swap
		Fitted $\blacktriangledown$ : The layout (including size and alignment) must be the same layout that was used to allocate that block of memory.	trait GlobalAlloc::dealloc
SystemIO	26	The variable is related to the system IO and depends on the target platform, including TCP sockets, handles, and file descriptors.	trait FromRawFd::from_raw_fd
Thread	2	Send: The type can be transferred across threads.	core::marker::Send
Thread	2	Sync: The type can be safe to share references between threads.	core::marker::Sync
Unreachable	5	The specific value will trigger unreachable data flow, such as enumeration index (variance), boolean value, etc.	impl¡T¿ Option¡T¿::unwrap_unchecked
Postcondition Safety Property
Aliased	32	Aliased $\blacktriangle$ : The value may have multiple mutable references or simultaneously have mutable and shared references.	impl¡T: ?Sized¿ *mut T::as_mut
		Mutated $\blacktriangledown$ : The value, which is owned by an immutable binding or pointed by shared reference, may be mutated.	impl¡T: ?Sized¿ *const T::as_ref
		Outlived $\blacktriangledown$ : The arbitrary lifetime (unbounded) that becomes as big as context demands may outlive the pointed memory.	impl CStr::from_ptr
DualOwned	46	It may create multiple overlapped owners in the ownership system that share the same memory via retaking the owner or creating a bitwise copy.	impl¡T: ?Sized¿ Box¡T¿::from_raw
Untyped	37	The value may not be in the initialized state, or the byte pattern represents an invalid value of its type.	core::mem::zeroed
Freed	19	The value may be manually freed or automated dropped.	impl¡T: ?Sized¿ ManuallyDrop¡T¿::drop
Leaked	35	The value may be leaked or escaped from the ownership system.	impl¡T: ?Sized¿ *mut T::write
Pinned	5	The value may be moved, although it ought to be pinned.	impl¡P: Deref¿ Pin¡P¿::new_unchecked