Pip
Architecture-dependent parts of Pip: MAL, IAL and boot
mal.h
Go to the documentation of this file.
1 /*******************************************************************************/
2 /* © Université de Lille, The Pip Development Team (2015-2021) */
3 /* */
4 /* This software is a computer program whose purpose is to run a minimal, */
5 /* hypervisor relying on proven properties such as memory isolation. */
6 /* */
7 /* This software is governed by the CeCILL license under French law and */
8 /* abiding by the rules of distribution of free software. You can use, */
9 /* modify and/ or redistribute the software under the terms of the CeCILL */
10 /* license as circulated by CEA, CNRS and INRIA at the following URL */
11 /* "http://www.cecill.info". */
12 /* */
13 /* As a counterpart to the access to the source code and rights to copy, */
14 /* modify and redistribute granted by the license, users are provided only */
15 /* with a limited warranty and the software's author, the holder of the */
16 /* economic rights, and the successive licensors have only limited */
17 /* liability. */
18 /* */
19 /* In this respect, the user's attention is drawn to the risks associated */
20 /* with loading, using, modifying and/or developing or reproducing the */
21 /* software by the user in light of its specific status of free software, */
22 /* that may mean that it is complicated to manipulate, and that also */
23 /* therefore means that it is reserved for developers and experienced */
24 /* professionals having in-depth computer knowledge. Users are therefore */
25 /* encouraged to load and test the software's suitability as regards their */
26 /* requirements in conditions enabling the security of their systems and/or */
27 /* data to be ensured and, more generally, to use and operate it in the */
28 /* same conditions as regards security. */
29 /* */
30 /* The fact that you are presently reading this means that you have had */
31 /* knowledge of the CeCILL license and that you accept its terms. */
32 /*******************************************************************************/
33 
39 #ifndef __MAL__
40 #define __MAL__
41 
42 #include <stdint.h>
43 
44 #include "maldefines.h"
45 
46 void enable_paging();
47 void disable_paging();
48 
49 /* Current page directory */
50 uint32_t getCurPartition(void);
51 void updateCurPartition (uint32_t descriptor);
52 
53 uint32_t getRootPartition(void);
54 void updateRootPartition (uint32_t descriptor);
55 
56 /* Address manipulation stuff */
57 uint32_t getNbIndex();
58 uint32_t getIndexOfAddr(uint32_t addr, uint32_t index);
59 uint32_t getOffsetOfAddr(uint32_t addr);
60 uint32_t readTableVirtual(uint32_t table, uint32_t index);
61 uint32_t readTableVirtualNoFlags(uint32_t table, uint32_t index);
62 uint32_t readArray(uint32_t table, uint32_t index);
63 void writeTableVirtual(uint32_t table, uint32_t index, uint32_t addr);
64 void writeTableVirtualNoFlags(uint32_t table, uint32_t index, uint32_t addr);
65 uint32_t readPresent(uint32_t table, uint32_t index);
66 void writePresent(uint32_t table, uint32_t index, uint32_t value);
67 uint32_t readAccessible(uint32_t table, uint32_t index);
68 void writeAccessible(uint32_t table, uint32_t index, uint32_t value);
69 uint32_t readPhysical(uint32_t table, uint32_t index);
70 uint32_t readPhysicalNoFlags(uint32_t table, uint32_t index);
71 void writePhysical(uint32_t table, uint32_t index, uint32_t addr);
72 void writePhysicalNoFlags(uint32_t table, uint32_t index, uint32_t addr);
73 uint32_t readIndex(uint32_t table, uint32_t index);
74 void writeIndex(uint32_t table, uint32_t index, uint32_t idx);
75 uint32_t dereferenceVirtual(uint32_t addr);
76 uint32_t derivated(uint32_t table, uint32_t index);
77 
78 uint32_t readPDflag(uint32_t table, uint32_t index);
79 void writePDflag(uint32_t table, uint32_t index, uint32_t value);
80 uint32_t get_pd();
81 
82 void cleanPageEntry(uint32_t table, uint32_t index);
83 
84 uint32_t defaultAddr(void);
85 extern const uint32_t defaultVAddr;
86 uint32_t getTableSize(void);
87 uint32_t getMaxIndex(void);
88 uint32_t addressEquals(uint32_t addr, uint32_t addr2);
89 void cleanPage(uint32_t paddr);
90 
91 uint32_t checkRights(uint32_t read, uint32_t write, uint32_t execute);
92 uint32_t applyRights(uint32_t table, uint32_t index, uint32_t read, uint32_t write, uint32_t execute);
93 
94 uint32_t toAddr(uint32_t input);
95 extern const uint32_t nbLevel;
96 
97 /* Amount of pages available, meh */
98 extern uint32_t maxPages;
99 #define nbPage maxPages
100 
101 /* Coq related stuff */
102 int geb(const uint32_t a, const uint32_t b);
103 int gtb(const uint32_t a, const uint32_t b);
104 int leb(const uint32_t a, const uint32_t b);
105 int ltb(const uint32_t a, const uint32_t b);
106 int eqb(const uint32_t a, const uint32_t b);
107 uint32_t mul3(uint32_t v);
108 uint32_t inc(uint32_t val);
109 uint32_t sub(uint32_t val);
110 uint32_t zero();
111 
112 
113 uint32_t indexPR(void);
114 uint32_t indexPD(void);
115 uint32_t indexSh1(void);
116 uint32_t indexSh2(void);
117 uint32_t indexSh3(void);
118 uint32_t PPRidx(void);
119 uint32_t kernelIndex(void);
120 void writePhysicalWithLotsOfFlags(uint32_t table, uint32_t index, uint32_t addr, uint32_t present, uint32_t user, uint32_t read, uint32_t write, uint32_t execute);
121 void writeKernelPhysicalEntry(uint32_t mmu_root_page, uint32_t kernel_index);
122 uint32_t extractPreIndex(uint32_t vaddr, uint32_t index);
123 
124 uint32_t prepareType(int b, uint32_t vaddr);
125 
126 
127 void updateMMURoot(page MMURoot);
129 bool noInterruptRequest(interruptMask flagsOnWake);
130 bool firstVAddrGreaterThanSecond(vaddr vaddr1, vaddr vaddr2);
131 contextAddr vaddrToContextAddr(vaddr contextVAddr);
132 bool checkIndexPropertyLTB(userValue userIndex);
133 index userValueToIndex(userValue userIndex);
135 vaddr getNthVAddrFrom(page base, uint32_t size);
136 void writeContext(contextAddr ctx, vaddr ctxSaveVAddr, interruptMask flagsOnWake);
137 void loadContext(contextAddr ctx, bool enforce_interrupts);
138 
139 #endif
void writePresent(uint32_t table, uint32_t index, uint32_t value)
Writes the present flag.
Definition: x86_multiboot/MAL/mal.c:299
void loadContext(contextAddr ctx, bool enforce_interrupts)
Definition: armv7/MAL/mal.c:448
unsigned int base
Base address.
Definition: gdt.h:97
void cleanPage(uint32_t paddr)
Cleans a given page, filling it with zero.
Definition: armv7/MAL/boot_requirements.c:141
uint32_t readTableVirtual(uint32_t table, uint32_t index)
FETCH address stored in indirection table.
Definition: armv7/MAL/mal.c:332
int gtb(const uint32_t a, const uint32_t b)
Greater than.
Definition: armv7/MAL/malinternal.c:153
uint32_t readTableVirtualNoFlags(uint32_t table, uint32_t index)
FETCH address stored in indirection table.
int eqb(const uint32_t a, const uint32_t b)
Equals.
Definition: armv7/MAL/malinternal.c:180
vaddr getNthVAddrFrom(page base, uint32_t size)
Definition: armv7/MAL/mal.c:397
uint32_t sub(uint32_t val)
Decrement an integer.
Definition: armv7/MAL/malinternal.c:198
uint32_t readPresent(uint32_t table, uint32_t index)
Reads the present flag.
Definition: armv7/MAL/mal.c:227
void writeContext(contextAddr ctx, vaddr ctxSaveVAddr, interruptMask flagsOnWake)
Definition: armv7/MAL/mal.c:425
uint32_t indexSh2(void)
Shadow 2 index within partition descriptor.
Definition: armv7/MAL/malinternal.c:106
uint32_t addressEquals(uint32_t addr, uint32_t addr2)
Checks whether an address is equal to another.
Definition: armv7/MAL/malinternal.c:135
contextAddr vaddrToContextAddr(vaddr contextVAddr)
Definition: armv7/MAL/mal.c:413
uint32_t index
Definition: armv7/MAL/include/maldefines.h:68
void writeTableVirtualNoFlags(uint32_t table, uint32_t index, uint32_t addr)
STORE an address in an indirection table.
uint32_t getMaxIndex(void)
Table size.
Definition: armv7/MAL/malinternal.c:216
uint32_t readAccessible(uint32_t table, uint32_t index)
Reads the accessible flag.
Definition: armv7/MAL/mal.c:157
#define userValue
Definition: armv7/MAL/include/maldefines.h:159
uint32_t getNbIndex()
Get amount of indirection tables.
Definition: armv7/MAL/mal.c:321
uint32_t addr
This is reserved by symbol table & ELF headers.
Definition: multiboot.h:68
uint32_t kernelIndex(void)
Index of kernel&#39;s page directory entry.
Definition: armv7/MAL/malinternal.c:61
void updateCurPartition(uint32_t descriptor)
Set current partition paddr.
Definition: armv7/MAL/mal.c:198
void cleanPageEntry(uint32_t table, uint32_t index)
Cleans a page entry, setting its contents to 0x00000000.
uint32_t checkRights(uint32_t read, uint32_t write, uint32_t execute)
Checks whether the asked rights are applicable to the architecture or not.
Definition: armv7/MAL/mal.c:350
uintptr_t vaddr
Definition: armv7/MAL/include/maldefines.h:59
uint32_t zero()
Zero. That&#39;s it.
Definition: armv7/MAL/malinternal.c:79
const uint32_t defaultVAddr
Default address, should be 0x00000000.
Definition: armv7/MAL/malinternal.c:46
uint32_t getIndexOfAddr(uint32_t addr, uint32_t index)
Get index of indirection level given.
Definition: armv7/MAL/mal.c:130
bool firstVAddrGreaterThanSecond(vaddr vaddr1, vaddr vaddr2)
Definition: armv7/MAL/mal.c:409
interruptMask getInterruptMaskFromCtx(contextAddr context)
Definition: armv7/MAL/mal.c:401
uint32_t getCurPartition(void)
Interface to get the current Page Directory.
Definition: armv7/MAL/mal.c:189
void writePhysicalWithLotsOfFlags(uint32_t table, uint32_t index, uint32_t addr, uint32_t present, uint32_t user, uint32_t read, uint32_t write, uint32_t execute)
Write a physical entry with all the possible flags we might need.
Definition: armv7/MAL/boot_requirements.c:159
int leb(const uint32_t a, const uint32_t b)
Lower or equal.
Definition: armv7/MAL/malinternal.c:162
uint32_t readIndex(uint32_t table, uint32_t index)
FETCH index stored in indirection table, physical version.
Definition: armv7/MAL/boot_requirements.c:95
uint32_t toAddr(uint32_t input)
Converts a given uint32_t to an address (only for Haskell FFI purposes)
Definition: armv7/MAL/boot_requirements.c:132
uint32_t indexSh1(void)
Shadow 1 index within partition descriptor.
Definition: armv7/MAL/malinternal.c:97
void disable_paging()
disables paging
Definition: armv7/MAL/mal.c:68
uint32_t readArray(uint32_t table, uint32_t index)
Read an array&#39;s contents.
uint32_t applyRights(uint32_t table, uint32_t index, uint32_t read, uint32_t write, uint32_t execute)
Apply the asked rights to the given entry.
uint32_t defaultAddr(void)
Default address, should be 0x00000000.
Definition: armv7/MAL/malinternal.c:52
void writePhysical(uint32_t table, uint32_t index, uint32_t addr)
STORE an address in an indirection table, physical version.
Definition: armv7/MAL/mal.c:81
index userValueToIndex(userValue userIndex)
Definition: armv7/MAL/mal.c:421
void writeIndex(uint32_t table, uint32_t index, uint32_t idx)
STORE an index in an indirection table, physical version.
Definition: armv7/MAL/boot_requirements.c:115
uint32_t maxPages
The maximal amount of pages available.
Definition: x86_multiboot/boot/mmu.c:51
uint32_t extractPreIndex(uint32_t vaddr, uint32_t index)
Definition: x86_multiboot/MAL/mal.c:477
vaddr getVidtVAddr()
Definition: armv7/MAL/mal.c:393
uint32_t readPDflag(uint32_t table, uint32_t index)
Reads the Page Directory flag into a shadow table.
Definition: armv7/MAL/mal.c:266
bool noInterruptRequest(interruptMask flagsOnWake)
Definition: armv7/MAL/mal.c:405
#define contextAddr
Definition: armv7/MAL/include/maldefines.h:155
const uint32_t nbLevel
Definition: armv7/MAL/mal.c:52
uint32_t size
This is reserved by symbol table & ELF headers.
Definition: multiboot.h:67
void writePDflag(uint32_t table, uint32_t index, uint32_t value)
Writes the page directory flag contents.
Definition: armv7/MAL/mal.c:249
uint32_t mul3(uint32_t v)
Multiply an integer with 3.
Definition: armv7/MAL/malinternal.c:207
uint32_t prepareType(int b, uint32_t vaddr)
Combines a boolean and a virtual address (boolean on the least significant bit)
Definition: armv7/MAL/mal.c:388
uint32_t indexPD(void)
Page directory index within partition descriptor.
Definition: armv7/MAL/malinternal.c:88
void writePhysicalNoFlags(uint32_t table, uint32_t index, uint32_t addr)
TODO.
Definition: armv7/MAL/mal.c:305
void writeKernelPhysicalEntry(uint32_t mmu_root_page, uint32_t kernel_index)
Writes the kernel MMU configuration page at index &#39;kernel_index&#39; in the MMU root page.
Definition: armv7/MAL/mal.c:374
uint32_t indexSh3(void)
Configuration tables linked list index within partition descriptor.
Definition: armv7/MAL/malinternal.c:115
uint32_t derivated(uint32_t table, uint32_t index)
Returns 1 if the page is derivated, 0 else.
bool checkIndexPropertyLTB(userValue userIndex)
Definition: armv7/MAL/mal.c:417
uint32_t dereferenceVirtual(uint32_t addr)
Definition: armv7/MAL/boot_requirements.c:206
void updateMMURoot(page MMURoot)
updates the virtual address space root page
Definition: armv7/MAL/boot_requirements.c:53
void writeTableVirtual(uint32_t table, uint32_t index, uint32_t addr)
STORE an address in an indirection table.
Definition: x86_multiboot/MAL/mal.c:419
int geb(const uint32_t a, const uint32_t b)
Greater or equal.
Definition: armv7/MAL/malinternal.c:144
uint32_t inc(uint32_t val)
Increment an integer.
Definition: armv7/MAL/malinternal.c:189
void updateRootPartition(uint32_t descriptor)
Set root partition paddr.
Definition: armv7/MAL/mal.c:216
uint32_t interruptMask
Definition: armv7/MAL/include/maldefines.h:142
uint32_t get_pd()
Returns the VIRTUAL ADDRESS of the current Page Directory.
uint32_t indexPR(void)
Partiton descriptor index into itself.
Definition: armv7/MAL/malinternal.c:70
void writeAccessible(uint32_t table, uint32_t index, uint32_t value)
Writes the accessible flag.
Definition: armv7/MAL/mal.c:176
uint32_t readPhysicalNoFlags(uint32_t table, uint32_t index)
Reads the address stored into table table, at index index, using physical addresses. This function masks the least significant bits that are used by the kernel to store various flags (see readVirEntry and readPhyEntry in model)
Definition: armv7/MAL/mal.c:102
uint32_t getTableSize(void)
Table size.
Definition: armv7/MAL/mal.c:119
void enable_paging()
enables paging
Definition: armv7/MAL/mal.c:58
uint32_t PPRidx(void)
Parent partition index within partition descriptor.
Definition: armv7/MAL/malinternal.c:124
uint32_t getOffsetOfAddr(uint32_t addr)
Get offset from address.
uint32_t present(uint32_t pd, uint32_t v)
Testing if a given virtual address is mapped or not into a virtual space.
Definition: properties.c:77
uintptr_t page
Definition: armv7/MAL/include/maldefines.h:53
int ltb(const uint32_t a, const uint32_t b)
Lower than.
Definition: armv7/MAL/malinternal.c:171
uint32_t getRootPartition(void)
Interface to get the current Page Directory.
Definition: armv7/MAL/mal.c:207
uint32_t readPhysical(uint32_t table, uint32_t index)
FETCH address stored in indirection table, physical version.
Definition: armv7/MAL/mal.c:285