tock / tock

A secure embedded operating system for microcontrollers
https://www.tockos.org
Other
5.41k stars 692 forks source link

allocate_app_memory_region needs to enforce alignment #1739

Open ppannuto opened 4 years ago

ppannuto commented 4 years ago

This came up in #1648: https://github.com/tock/tock/pull/1648#discussion_r402822448

Basically, this is working out fine right now because all the MPU region allocators do allocate regions larger than the pointer size (which is certainly unlikely to change). Nonetheless, we have an unexpressed requirement here that we should capture.

ia0 commented 1 year ago

This is only working out fine right now as long as a custom MPU implementation is used. The default implementation does not enforce any alignment.

Here's the bug (undefined behavior when the default implementation of allocate_app_memory_region is used): https://github.com/tock/tock/blob/6e0aeb0328a114775ce301bac48682173a54a4bd/kernel/src/process_standard.rs#L1666-L1679

Here's the default implementation breaking the invariant the unsafe code above relies on: https://github.com/tock/tock/blob/6e0aeb0328a114775ce301bac48682173a54a4bd/kernel/src/platform/mpu.rs#L221-L240

Also, it looks like the documentation of allocate_app_memory_region does not guarantee alignment, so the code in ProcessStandard::create() is actually assuming things it should not.

hudson-ayers commented 1 year ago

Did you hit this bug in practice? If so I am curious to see how. I guess just using the default MPU config on a board with no MPU?

I agree that we should update the documentation for allocate_app_memory_region() and the default implementation to guarantee these constraints.

ia0 commented 1 year ago

Did you hit this bug in practice? If so I am curious to see how. I guess just using the default MPU config on a board with no MPU?

Yes, I've hit this bug in practice (the kernel panics with an Unaligned Access Usage Fault). Indeed, I'm using the default MPU config (the board could have an MPU, but the layout constraints imposed by Tock and the MPU are too restrictive). I don't have a minimal reproduction example, but to get you an idea here's how one could be forged:

static BUSY: AtomicBool = AtomicBool::new(false);
static COUNTER: AtomicU32 = AtomicU32::new(0);
pub fn start_work(...) {
    assert!(!BUSY.swap(true, SeqCst)); // must not already be running
    COUNTER.fetch_add(1, SeqCst);
    ...
}
pub fn stop_work(...) {
    assert!(BUSY.load(SeqCst)); // must be running
    ...
    BUSY.store(false, SeqCst);
}

Depending on how stars are aligned (essentially the rest of the code and possibly completely unrelated parts), the compiler may decide to order BUSY and COUNTER differently. If those are the only symbols in .bss and .data is empty, then the RAM usage may either be: