e22089d0cc
When the kernel is built the build system is responsible for finding a suitable physical memory location where the kernel can be put on the given target platform. This is recorded into the kernel.elf file and read by the elfloader program when it loads the kernel to that memory address. In order to find memory blocks to avoid, the build system looks for the /reserved-memory node in the target platform's device tree dts, along with other device memory blocks. The bcm2837 / Raspberry Pi 3 bootloader uses the first memory page at address 0x0 to load a so called armstub which is used to set up the ARM processor's initial state. It is also used to "park" the secondary cores by putting them in a spin loop located within the armstub from which the boot core can release them when ready. The rpi3.dts already contains a /memreserve/ node reserving this page, however as the build system only looks for the standardized reserved-memory node it promptly disregards it and allow the kernel to be loaded at physical address 0x0, overwriting the armstub. A side effect of this is that the spinloop code also is overwritten, potentially releasing the secondary cores to execute whatever kernel code is written in the place of their spinloops, causing all kinds of undefined behavior dependent on both race conditions and kernel elf layout. It also implies that the kernel SMP boot code would not be able to release the cores if implemented for the platform. This patch adds the /reserved-memory node to the overlay-rpi3.dts file and a child node reserving the memory region for the first memory page. This in effect causes the kernel to instead be loaded to 0x1000000 (aligned to a supersection). Co-authored-by: Axel Heider <axelheider@gmx.de> Signed-off-by: Viktor Sannum <sannum.viktor@gmail.com> |
||
|---|---|---|
| .github/workflows | ||
| .reuse | ||
| configs | ||
| include | ||
| libsel4 | ||
| LICENSES | ||
| manual | ||
| src | ||
| tools | ||
| .cmake-format.yaml | ||
| .gitignore | ||
| .licenseignore | ||
| CAVEATS-generic.md | ||
| CAVEATS-ia32.md | ||
| CHANGES | ||
| CMakeLists.txt | ||
| CODE_OF_CONDUCT.md | ||
| config.cmake | ||
| CONTRIBUTING.md | ||
| CONTRIBUTORS.md | ||
| FindseL4.cmake | ||
| gcc.cmake | ||
| gdb-macros | ||
| LICENSE.md | ||
| llvm.cmake | ||
| README.md | ||
| SECURITY.md | ||
| VERSION | ||
The seL4 microkernel
This project contains the source code of seL4 microkernel.
For details about the seL4 microkernel, including details about its formal
correctness proof, please see the sel4.systems website and associated
FAQ.
DOIs for citing recent releases of this repository:
We welcome contributions to seL4. Please see the website for information on how to contribute.
This repository is usually not used in isolation, but as part of the build system in a larger project.
seL4 Basics
- Tutorials
- Documentation
- seL4 libraries
- seL4Test
- Debugging guide
- Benchmarking guide
- Virtualization on seL4
- Host Build Dependencies
- Porting seL4
Community
See the contact links on the seL4 website for the full list.
Reporting security vulnerabilities
If you believe you have found a security vulnerability in seL4 or related software, we ask you to follow our vulnerability disclosure policy.
Manual
A hosted version of the manual for the most recent release can be found here.
A web version of the API can be found here
Repository Overview
includeandsrc: C and ASM source code of seL4tools: build toolslibsel4: C bindings for the seL4 ABImanual: LaTeX sources of the seL4 reference manual
Build Instructions
See the seL4 website for build instructions.
Status
A list of releases and current project status can be found under seL4 releases.
- Roadmap: new features in development
- Hardware Support: information about hardware platform ports
- Kernel Features: information about available kernel features
- Userland Components and Drivers: available device drivers and userland components
License
See the file LICENSE.md.