CuBit
1.0.0
Cubitos ist ein Multi-Prozessor, 64-Bit, (teilweise) formell verifiziert, allgemeines Betriebssystem, derzeit für die X86-64-Architektur.
Kubit ist im Funkendialekt von ADA geschrieben.
Kubit ist sehr viel Arbeit! Trotzdem drehen Sie es bitte. Mitwirkende Willkommen!
gprbuild , gnat usw. in Ihrem $PATHUm bootfähige. ISO zu erstellen, benötigen Sie auch:
Abhängigkeiten: Sie benötigen den Gnat 2020-Compiler, und wenn Sie die Live-CD erstellen möchten, benötigen Sie die Xorriso- und Grub-Mkrescue- Tools sowie möglicherweise GRUB-PC-BIN, je nachdem, welche Emulator/Virtualisierungsumgebung Sie verwenden. Diese werden wahrscheinlich im Paketmanager Ihrer Distribose bereitgestellt. Dies kann unter Verwendung von WSL in Linux und unter Windows eingebaut werden.
git clone https://github.com/docandrew/CuBit.git
make
Dadurch wird Kubit erstellt und eine Live-CD-.ISO-Datei erstellt. Die ISO kann montiert und in Virtualbox, Bochs oder QEMU ausgeführt werden.
| Aufgabe | Befehl |
|---|---|
| Dokumentation erstellen (in Build/Dokumenten) | make docs |
| Provers laufen | make prove |
| Erstellen Sie HTML -Dokumentation | make html |
ADA ist von Fall unempfindlich (was ehrlich gesagt nett ist), aber alle exportierten Symbole unterkasieren, so dass alles in Dateien, auf die sich das Symbol verweist, die niedrigere Version verwenden oder den externen Namen für das Symbol in einem Aspekt angeben muss.
Aufzählte Typen, die "Löcher" enthalten, führen dazu, dass GNAT bei der Zuweisung dieser Laufzeitprüfungen für gültige Werte einfügt. Ich konnte keine Pragma finden, um diese Schecks zu deaktivieren. Schließlich schreiben wir Ausnahmebehandlerfunktionen, die entweder die Schecks ausführen oder eine Kernel -Panik verursachen können, aber im Moment die Löcher mit offensichtlichen Werten wie Bad_1, Bad_2 usw. füllen.
Bitte stellen Sie sicher, dass Beweise ausgeführt werden (mit make prove ), bevor Sie Pull -Anfragen einreichen. Seien Sie sehr vorsichtig, wenn Pragma kommentiert wird, um Warnungen zu deaktivieren. gnatprove wird einige falsche Warnungen geben, die eine ähnliche statement has no effect oder unused assignment , die eindeutig falsch sind, aber bitte überprüfen Sie diese.
Variantenaufzeichnungen scheinen zusätzliche Kreuzungen in den zugrunde liegenden Datensatz aufzunehmen, auch wenn das Pragma -Paket verwendet wird. Verwenden Sie diese nicht als "Overlays" über vorhandenen Speicher, z. B. die ACPI -Tabellen. Sie haben Ausrichtungsprobleme mit einigen Feldern und enden mit Junk -Daten. Gleiches gilt auch für nicht variante Aufzeichnungen, die Diskriminanten verwenden.
MAX_PHYS_ALLOC - In config.ads eingestellt ist, ist dies der maximale physische Speicher, den Cubit unterstützt. Hier ist nur ein Grenzwert praktisch, da der Boot -Mem -Allocator eingerichtet ist, um Bitmaps für all diesen Speicher (128 GIB) zu erstellen, der eine ganze Menge Platz einnimmt. (Wir können in Betracht ziehen, nur einen kleinen, linear angeordneten Haufen für den Kernelgebrauch beiseite zu legen und einen besseren Allocator zu erstellen, sodass diese Grenze kein Faktor mehr ist.)
MAX_PHYS_ADDRESS - Der maximale theoretische physische Speicher, den unsere Hardware unterstützt (wenn wir eine lineare Zuordnung verwenden). Im Fall von x86-64 haben wir kanonische 48-Bit-virtuelle Adressen. Wenn wir also möchten, dass das gesamte physische Speicher im virtuellen Speicher abgebildet wird, haben wir ungefähr 280 TB, was wir uns in der höheren Halbzeit teilen müssen, also 128tib. Beachten Sie, dass Intel eine 56-Bit-Adressierung mit einer Seitentabelle mit fünf Ebenen untersucht, sodass sich diese Nummer für X86-64 bald ändern kann.
MAX_PHYS_ADDRESSIBLE - Die oberste physische Speicheradresse in unserem System , die wir zur Laufzeit erkennen. Bis zu diesem Zeitpunkt linear-Map-Speicherbereiche (ab 0xffff_8000_0000_0000).
MAX_PHYS_USABLE - Die oberste verwendbare RAM -Adresse in unserem System . Es kann Löcher darin enthalten, sodass wir nicht blind von dieser Grenze von dieser Grenze zuweisen können, aber von einem physischen Allocator wird erwartet, dass er bis zu diesem Punkt Adressen behandelt.
Einige der verwendeten Strukturen, wie die GDT- und Seitentabellen, müssen vor dem Umschalten in den langen Modus im boot.asm eingerichtet werden. Diese werden als "Bootstrap" -GDT- bzw. Seitentabellen bezeichnet. Es gibt auch den "Boot" -Prosgallocator für physischen Speicher. Später haben wir die Gesamtheit des physischen Gedächtnisses in die höhere Hälfte des Kernels zusammen mit einem neuen GDT in segment.adb neu auf. Diese werden als "Kernel -Seitentabellen" und "Kernel Gdt" bezeichnet.
Die Bootstrap-Tabellen-Identitäts-Map Die ersten 1 g Speicher und dann erneut in die höhere Hälfte abzuordnen, beginnend bei 0xffff_8000_0000_0000. Also wirkt der P2V und V2P (physikalisch zu virtuell, virtuell-physical) nach einfacher Addition und Subtraktion, da Sie auf den physischen Speicher zugreifen können, beispielsweise 0x0000_0000_dead_beeef unter den virtuellen Adressen 0x0000_0000_dead_beef und auch 0xffff.8000_dead_beef.
Wenn wir zur Kernel -Karte wechseln, können wir den Speicher nicht mehr mit direkten physischen Adressen addieren. Stattdessen muss auf eine bestimmte physische Adresse unter Verwendung der linear-kartierenden Adresse unter 0xffff_8000_0000_0000 zugegriffen werden. Wir haben den gesamten physischen Speicher linear-Map in 0xffff_8000_0000_0000 bis 0xffff_8fff_ffff_ffff.
Beachte Daher benötigen unsere Seitentabellen auch eine Zuordnung für 0xffff_ffff_8xxx_xxxx -> 0x0000_0000_0xxx_xxxx.
Ja! Ich habe versucht, den Code sehr freundlich zu denjenigen zu machen, die mit Cubitos, Ada oder Spark nicht vertraut sind. Bitte probieren Sie es mit einer VM aus und lassen Sie mich wissen, was Sie denken. Negative Rückmeldungen und konstruktive Kritik sind ebenfalls nützlich.
Es ist stark dokumentiert und Mitwirkende sind willkommen!
Cubitos ist möglicherweise ein guter Ausgangspunkt für die akademische Forschung. Spark hat eine Fluchtluke, um Beweise im CoQ durchzuführen. Für die mathematischeren Mitwirkenden, die eine gute Herausforderung wollen, sehen Sie, was Sie über Cubitos beweisen können!
Spark verwendet das WHY3 -Framework und den Z3 Smt Solver. Gute, schnelle SMT-Löser sind immer ein Interessengebiet, und Cubitos könnte eine gute Möglichkeit sein, sie für andere reale Verwendungen zu belasten.
| Codeelement | Konvention |
|---|---|
| ADA -Schlüsselwörter (Typ, für, Schleife usw.) | Alle Kleinbuchstaben |
| Typen (MultibootStruct, PagetableEntry usw.) | Kapitalisierte Kamelbezug |
| Paketnamen | Kapitalisierte Kamelbezug |
| Variablen, Funktionen (Kmain, TohexString usw.) | Unkapitalisiertes Kamelbezug |
| Konstanten (LT_GRAY, KERN_BASE usw.) | Alle Kappen |
| Dateinamen | Alle unteren oder Snake_Case |
HINWEIS: Wenn Sie eine externe Komponente anstellen, z. B. Multiboot, sollten die Variablennamen dieselbe Konvention wie die API dieser Komponente verwenden. Zum Beispiel enthält die Multiboot -Info -Struktur Felder wie Mem_lower usw.
Wir werden diese Namen hier wörtlich verwenden, um eine Leichtigkeit der Dokumentationsreferenz zu erhalten. Dies ist keine harte und schnelle Regel. Wenn die API-Namen übermäßig Terrassen, verwirrend sind, eine seltsame ungarische Notation verwenden oder ansonsten dumm sind, können Sie sie im ADA-Code umbenennen.
Vermeiden Sie übermäßig Terrassenabkürzungen. Gemeinsame Begriffe wie "Kern" für "Kernel" oder "Mem" für das Gedächtnis sind in Ordnung, wenn es keine Unklarheit gibt. "VM" für virtuelles Gedächtnis kann mit "virtueller Maschine" verwechselt werden. Bevorzugen Sie also "VirtMem" oder buchstabieren Sie es einfach vollständig. Akronyme sollten nur verwendet werden, wenn sie weit verbreitet sind oder eine Konvention der zugrunde liegenden Hardware wie ACPI.
Bitte wandeln Sie Registerkarten in vier Leerzeichen um.
Commits sollten LF -Linienende sein.
Vermeiden Sie "Verwenden Sie" Klauseln, sofern für die Bediener nicht etwas anderes erforderlich ist, und beschränken Sie ihre Verwendung dann auf bestimmte Unterprogramme, wenn dies erforderlich ist, oder verwenden Sie die Klausel "Verwendung Typ". Dadurch wird das Paket eines Typs ausdrücklich dargelegt, und so kann das Paket in einem Editor leicht referenziert und zugesprungen werden. Ausnahmen zu dieser Regel sind:
Verwenden Sie den Begriff "Frame", wenn Sie sich auf den physischen Speicher und "Seite" beziehen, wenn Sie den virtuellen Speicher besprechen.
Bitte verwenden Sie beschreibende Namen für Variablen, Typen usw. Wir fehlen nicht nach Festplattenraum, um den Quellcode zu speichern. Verwenden Sie also längere Namen (innerhalb von Grund), wenn sie dazu beitragen, das Verständnis des Codes zu fördern.
Versuchen Sie, zum größten Teil die Linien weniger als 80 Chars breit zu halten. Wenn dies jedoch die Lesbarkeit zum Brechen einer Linie beeinflusst, ist es in Ordnung, die 80-breite Limit zu sprengen. Das Ende der Zeilenkommentare können über 80 hinausgehen, wenn es den Fluss des Codes verletzt, um sie in ihre eigene Zeile zu setzen.
Wenn der Spark -Modus in einem Subprogramm -Körper deaktiviert ist, fügen Sie bitte einen Kommentar hinzu, warum. Dies kann vollkommen gültig sein, dh Inline ASM. Versuchen Sie jedoch, den Code umzustrukturieren, um den Spark -Modus zu aktivieren - insbesondere Subprogrammspezifikationen. Manchmal kann dies ein wenig schmerzhaft sein, dh die Änderung der Funktionen in Verfahren mit mehreren "Out" -Paramien.
Feiern Sie Weißespace. Lassen Sie den Code atmen. Verwenden Sie nach jedem Subprogrammkörper zwei neue Zeilen. Eine neue Linie nach einem Subprogramm -Körper ist angemessen, wenn die Unterprogramme geringfügige Variationen voneinander sind, dh überlastete Argumente, und sie sind eng gruppiert, um ihre Beziehung zu klären.
Verwenden Sie viele Kommentare im Gnatdoc -Format. Dies ist offensichtlich ein Bereich, in dem sich die Meinungen unterscheiden, aber ich glaube, dass die Behandlung des Betriebssystems wie eine Bibliothek mit gründlicher Dokumentation die Korrektheit fördert und es neuen Mitwirkenden freundlicher macht. Dies erleichtert auch die automatische Generate-Dokumentation, anstatt die Dokumentation separat beizubehalten. Wir alle kennen eine gute API, wenn wir eine sehen.
"Aber der Code wird sich ändern und die Kommentare werden veraltet sein!"
Also ... ähm ... aktualisiere einfach die Kommentare!
Ausleihen einer Seite von Flugzeugbetreiberhandbüchern:
HINWEIS - Zeigt Informationen an, die als wichtig angesehen werden, um hervorzuheben
Achtung - Bezeichnet Informationen, die, falls dies nicht in Betracht gezogen werden, zu Systemabstürzen oder einem falschen Betrieb führen können.
WARNUNG - Bezeichnet Informationen, die, falls dies nicht in Betracht gezogen werden, zu einem Verlust von Benutzerdaten oder zu einer Beschädigung der zugrunde liegenden Hardware führen können.
| Begriff verwendet | Größe |
|---|---|
| Knabbern | 4 Bit |
| Byte | 8 Bit |
| Wort | 16 Bit |
| DWORD (Doppelwort) | 32 Bit |
| QWord (Quad-Wort) | 64 Bit |
Dies ist hier enthalten, um die Verwirrung zu vermeiden, die bei der Beschreibung von Schnittstellen oder Hardwarekomponenten verwendet wird, bei denen "Wort" etwas anderes als 16 Bit bedeuten kann. Wir meinen immer 16 Bit im Cubit-Code, wenn wir in Kommentaren "Wort" usw. verwenden, usw.
Im Allgemeinen werden wir die Länge eines Datentyps mithilfe des ADA-Schnittstellenpakets dh unsigned_8, unsigned_32 usw. ausdrücklich angeben.
Sparkfunktionen dürfen keine Nebenwirkungen haben, so oft wird stattdessen ein Verfahren verwendet, und ein Out-Parameter für das Ergebnis ist erforderlich, anstatt nur das Ergebnis zurückzugeben. Es ist ein bisschen schmerzhaft, für alle Verfahrensergebnisse temporäre zuzuweisen.
Definitionen von Konstanten können nicht (leicht) zwischen dem ADA -Code und den Montagedateien geteilt werden, sodass einige von ihnen dupliziert werden. Ich habe versucht, alle Konstanten von den Montagedateien in Cubit.inc zu verwenden, zusammen mit einer Notiz, wo sie möglicherweise in ADA -Code dupliziert werden. Bitte stellen Sie sicher, dass sie an beiden Orten geändert werden, wenn Sie einen dieser Werte ändern. Wenn Sie Ihre eigene Konstante vorstellen, die zwischen Montage und ADA -Code geteilt wird, stellen Sie sicher, dass sie denselben Namen verwenden!
Kubit unterteilt den statischen Stapelbereich in Per-CPU-Stücke, von denen jedes in die primären und sekundären Stapel für diese CPU aufgeteilt wird. Der primäre Stapel wächst, der Sekundärstapel wächst. Der primäre Stapelzeiger ist für die Haupt -CPU in boot.asm eingestellt und für jede zusätzliche CPU eingestellt, wenn sie in boot_ap.asm starten.
STACK_TOP +-----------------------+
| |
| CPU 0 Primary Stack |
| |
+-----------------------+
| CPU 0 Secondary Stack |
+-----------------------+
| |
| CPU 1 Primary Stack |
| |
+-----------------------+
| CPU 1 Secondary Stack |
+-----------------------+
| . |
| . |
| . |
+-----------------------+
| |
| CPU N Primary Stack |
| |
+-----------------------+
| CPU N Secondary Stack |
STACK_BOTTOM +-----------------------+
Der sekundäre Stack SS_init-Anruf wird während jedes CPU-Start-ups getätigt. Sekundärstapelüberläufe sollten zur Laufzeit erkannt werden, sind jedoch Vorsicht geboten. Während der Systeme und Interrupts kann der Kernel -Stapel des Prozesses verwendet werden, der keinen sekundären Stapel hat.
X bedeutet fertig- bedeutet in Arbeit [ ] There are a lot of potential circular dependencies for just "proof stuff",
i.e. preconditions where we don't want to call a blockingSleep until
interrupts are enabled -> don't want to enable interrupts until the
interrupt vector is loaded -> interrupt vector will update the value that
blockingSleep depends on. It might make sense to keep a big "state"
.ads file with nothing but Ghost variables used in SPARK proofs. It would
not have any dependencies itself, but could be included by everything else
to update their states. Downside is that it might grow huge and unwieldy,
and sorta breaks encapsulation. Might make proofs take a long time too.
[X] Put the stack at a more sensible location
[X] Per-CPU Stacks
[X] Secondary Stacks
[X] Print out full register dump with exceptions
[-] Make type-safe more of the address/number conversions I'm doing.
[-] Error-handling. Need to formalize the mechanism, could get very messy with MP.
[X] Exceptions (Last chance handler)
[ ] Broadcast panic to other CPUs
[ ] Figure out a keyboard scancode -> key array scheme with a future eye towards
internationalization. Maybe just use SDL's keyboard handling scheme and let them sort it out.
[X] Physical memory allocator
[X] Boot-mem allocator using bitmaps
[X] Boot phys memory allocator
[X] Keep track of free space as we allocate/free
[X] Buddy allocator
[X] Virtual memory mapper
[X] Mark 0 page as not present
[X] Re-map kernel pages with appropriate NXE bits, etc. depending on region.
[-] Virtual memory allocator
[-] Demand paging.
[-] Processes / Threads
[ ] Kernel Tasks
[X] Usermode
[-] Scheduler
[ ] Implement killing processes.
[ ] Suspend
[ ] Sleep / Wakeup
[-] ACPI tables
[X] Find RSDT/XSDT
[X] Sane code for parsing these.
[-] APIC
[ ] HPET
[ ] MCFG - PCI express
[ ] SSDT?
[-] I/O APIC
[-] Multiprocessing
[ ] MP Tables (necessary?)
[-] LAPIC
[ ] X2APIC
[ ] Hardware
[X] MSRs
[-] Full CPUID detection
[-] Disk drivers
[ ] MBR/GPT Partition Table
[-] PCI bus
[-] Hard Drives
[-] ATA
[-] AHCI
[ ] PCI express
[ ] Enhanced Configuration Access Mechanism (ECAM) via MCFG tables
[ ] NVMe
[ ] Sound
[ ] Video Drivers
[-] VESA Modes
[-] Filesystem / VFS Layer
[ ] Develop FS-agnostic set of VFS hooks to syscalls
[ ] Develop Drive-agnostic set of VFS hooks to hardware
[-] Ext2
[ ] Networking
[ ] Interface driver
[ ] TCP/IP Stack - RecordFlux should help here.
[ ] Security
[ ] ASLR / KASLR
[ ] Disable certain branch speculation behavior (see x86.MSR)
[ ] if processor supports IBRS in ARCH_CAPABILITIES
[-] KPTI
[ ] Disable KPTI if ARCH_CAPABILITIES MSR indicates not susceptible to RDCL
[ ] Sensible Kernel-Mode-Setting / Framebuffer / Compositor arrangement
[ ] Wow Factor / Eye Candy
[ ] Sweet GRUB splash screen w/ logo
[-] Syscalls
[X] SYSCALL/SYSRET working
[ ] Microkernel Concepts?
[ ] User-mode drivers?
[ ] IPC?
[-] More formal proofs of kernel correctness
[ ] Preventing race conditions - may not be feasible outside of
Ravenscar profile, which doesn't really apply to us.
[-] Implement more of the Ada standard library, especially for Tasks.
[-] Init model - should this look like UNIX? Something else?
[ ] Security Model
[-] Codify it
[ ] Prove it
[ ] Implement it
[-] IMGUI framework
[-] Make all package names Uppercase
[-] Rename all setupXYZ to just setup, since package name is already there.
[X] New Makefile
[-] Use gnatdoc format in comments
[ ] Edit gnatdoc format so NOTE, CAUTION, WARNING shows up as different
colors.
[ ] Edit gnatdoc format to ignore the leading and trailing horizontal rules
[-] Work out a CI/CD pipeline
[ ] Proof Step
[ ] Unit Testing
[X] Build
[ ] Integration/Functional Testing
[X] Generate Documentation
[-] Build installers, isos, etc.
[ ] Write unit tests
[ ] Fuzzing
[ ] Integration tests that run in the OS.
| Aufgabe | Befehl |
|---|---|
| Dokumentation erstellen (in Build/Dokumenten) | make docs |
| Provers laufen | make prove |
| Erstellen Sie HTML -Dokumentation | make html |
Sie können ein Ext2 -Datenträgerbild erstellen und es mit diesen Befehlen in Cubit lesen, die hier für eine 128 -MB -Festplatte angezeigt werden:
dd if=/dev/zero of=vhd.img bs=1M count=128
mkfs -t ext2 -b 4096 vhd.img
mkdir vhd
mount -t auto -o loop vhd.img vhd
Jetzt haben Sie ein leeres Dateisystem in vhd/ , zu dem Sie Dateien hinzufügen können, mit Berechtigungen herumspielen usw., wenn Sie fertig sind, das Bild entschärfen. Beachten Sie, dass die Ext2 -Implementierung von Cubit derzeit nur 4K -Blockgrößen unterstützt.
umount vhd
Jetzt haben Sie ein Festplattenbild, mit dem Sie in das VirtualBox -Format konvertieren können:
VBoxManage convertfromraw --format VDI vhd.img vhd.vdi
Sie können die neue Festplatte unter Speicher -> IDE -Controller in Ihren VM -Einstellungen hinzufügen. Sie möchten wahrscheinlich den ICH6 -Chipsatz verwenden. Cubit verwendet derzeit die alte PIO -Methode für ATA I/O. Wenn Sie ein Festplattenbild erstellen und es dem IDE -Controller mit einem anderen Chipsatz hinzufügen, werden die Lesevorgänge wahrscheinlich fehlschlagen.
Beachten Sie, dass Cubit gerade den EXT2 -Superblock derzeit liest. Der Fortschritt wird jedoch mit dem Basis -Dateisystemunterstützung erzielt.
Bitte experimentieren Sie mit verschiedenen RAM -Mengen, Anzahl der CPUs usw.
VirtualBox ist ein gutes Tool zum Testen. QEMU ist jedoch schön, wenn Sie GDB verwenden müssen, um bestimmte Probleme aufzuspüren. Beachten Sie, dass Cubit einige ziemlich aktuelle CPU -Funktionen verwendet, sodass Sie QEMU sagen möchten, dass sie einen neueren Chipsatz und eine CPU verwenden sollen. Die Optionen -machine q35 und -cpu Broadwell scheinen gut zu funktionieren.
QEMU -Befehl mit Debugger:
qemu-system-x86_64 -machine q35 -cpu Broadwell -m 64M -cdrom path/to/cubit_kernel.iso
GDB -Tipps:
Register Add'l Info: rt Register: rg64 Stack Trace: k
Verwenden Sie QEMU zum Debuggen:
qemu-system-x86_64 -machine q35 -cpu Broadwell -s -S -m 4G -cdrom pathtocubit_kernel.iso -serial stdio
Qemu wird in einem pausierten Zustand beginnen, während es auf den Debugger wartet.
Dann führen Sie GDB: gdb cubit_kernel (Hinweis: Nein ".ISO" Hier möchten wir die Kernel -Objektdatei selbst, die Debugging -Symbole enthält).
Um eine Verbindung zu QEMU herzustellen: target remote localhost:1234 Verwendung (gdb) c , um fortzufahren.
Von hier aus funktionieren normale GDB -Befehle wie break , x usw.
Beachten Sie, dass Hyper-V den. ISO derzeit nicht zu starten scheint. Andere Virtualisierungs- oder Emulationsplattformen werden empfohlen.
git clone https://github.com/Componolit/RecordFlux
install >= Python 3.6
install pip
install virtualenv if Python 3 not the default
source bin/activate
python setup.py build
python setup.py install
Now the rflx script at bin/rflx should work.
