diff --git a/submissions/guillermovidalsule/README.md b/submissions/guillermovidalsule/README.md new file mode 100644 index 0000000..c207bda --- /dev/null +++ b/submissions/guillermovidalsule/README.md @@ -0,0 +1,69 @@ +# Physical Memory Protection - Configuration Verifier + +This purpose of this tool is to verify whether a given access +with privilege mode _M_ can undertake an operation of type _O_ +at a specific address. + +## Project Structure + +The folders and files are the following: + +| Name | Type | Description | +| :--- | :---: | :---------- | +| `bin` | Directory | Output directory where the executable is placed. | +| `config` | Directory | Further configuration of the project. | +| `src` | Directory | Source code. | +| `alire.toml` | File | Crate settings. | +| `configuration.txt` | File | Basic PMP configuration to test the program. | +| `pmp_check.gpr` | File | Project configuration file. | +| `README.md` | File | Informational README about the project. | + +There could be more entries, but they are out of the scope for the coding challenge. + +The most important part is the source code, which consists of: + +1. `pmp_check.adb` - Main program. +2. `pmp.ads` - Description of the PMP system. +3. `pmp.adb` - Implementation of the PMP system. + +## Compile + +In order to run the program you will need `gprbuild`. You can download it +with the GNAT FSF toolchain, which includes other necessary packages. + +``` +project-dir$ gprbuild -P pmp_check.adb +``` + +Alternatively, if you have the toolchain set up with Alire: + +``` +project-dir$ alr build +``` + +## Run + +Running it is as simple as: + +``` +project-dir$ ./bin/pmp_check
+``` + +> [!NOTE] +> If you do not wish / cannot compile it, a binary is already provided at the bin directory, but it can only be run on a x86\_64 architecture. + +## Tools + +I used the GNAT FSF 14 toolchain paired with Alire. In particular: + +- `gprbuild 22.0.0` +- `alr 2.0.2` +- `gcc 14.2.0` (precompiled version that came with the toolchain) + +This does not imply that other versions will not work, you could even try +using `gnatmake`, but I will not verify whether they are compatible or not. + +## Final Remarks + +I chose Ada because it is a statically and strongly typed language like IDL, + which is mentioned in the project description. diff --git a/submissions/guillermovidalsule/alire.toml b/submissions/guillermovidalsule/alire.toml new file mode 100644 index 0000000..ebb8600 --- /dev/null +++ b/submissions/guillermovidalsule/alire.toml @@ -0,0 +1,12 @@ +name = "pmp_check" +description = "" +version = "0.1.0-dev" + +authors = ["Guillermo Vidal Sulé"] +maintainers = ["Guillermo Vidal Sulé "] +maintainers-logins = ["github-username"] +licenses = "MIT OR Apache-2.0 WITH LLVM-exception" +website = "" +tags = [] + +executables = ["pmp_check"] diff --git a/submissions/guillermovidalsule/alire/alire.lock b/submissions/guillermovidalsule/alire/alire.lock new file mode 100644 index 0000000..d08d4b6 --- /dev/null +++ b/submissions/guillermovidalsule/alire/alire.lock @@ -0,0 +1,6 @@ +# THIS FILE IS GENERATED. DO NOT EDIT. + +[solution] +[solution.context] +solved = true + diff --git a/submissions/guillermovidalsule/alire/build_hash_inputs b/submissions/guillermovidalsule/alire/build_hash_inputs new file mode 100644 index 0000000..0e488a1 --- /dev/null +++ b/submissions/guillermovidalsule/alire/build_hash_inputs @@ -0,0 +1,4 @@ +external:LIBRARY_TYPE=default +external:PMP_CHECK_LIBRARY_TYPE=default +profile:pmp_check=DEVELOPMENT +switches:pmp_check=-Og,-fdata-sections,-ffunction-sections,-g,-gnatVa,-gnatW8,-gnatw.X,-gnatwa,-gnaty-d,-gnaty3,-gnatyA,-gnatyB,-gnatyI,-gnatyO,-gnatyS,-gnatya,-gnatyb,-gnatyc,-gnatye,-gnatyf,-gnatyh,-gnatyi,-gnatyk,-gnatyl,-gnatym,-gnatyn,-gnatyp,-gnatyr,-gnatyt,-gnatyu,-gnatyx diff --git a/submissions/guillermovidalsule/alire/flags/post_fetch_done b/submissions/guillermovidalsule/alire/flags/post_fetch_done new file mode 100644 index 0000000..e69de29 diff --git a/submissions/guillermovidalsule/alire/settings.toml b/submissions/guillermovidalsule/alire/settings.toml new file mode 100644 index 0000000..53b9f80 --- /dev/null +++ b/submissions/guillermovidalsule/alire/settings.toml @@ -0,0 +1,2 @@ +last_build_profile = "pmp_check=DEVELOPMENT" + diff --git a/submissions/guillermovidalsule/bin/pmp_check b/submissions/guillermovidalsule/bin/pmp_check new file mode 100755 index 0000000..69215df Binary files /dev/null and b/submissions/guillermovidalsule/bin/pmp_check differ diff --git a/submissions/guillermovidalsule/config/pmp_check_config.ads b/submissions/guillermovidalsule/config/pmp_check_config.ads new file mode 100644 index 0000000..30157e9 --- /dev/null +++ b/submissions/guillermovidalsule/config/pmp_check_config.ads @@ -0,0 +1,20 @@ +-- Configuration for pmp_check generated by Alire +pragma Restrictions (No_Elaboration_Code); +pragma Style_Checks (Off); + +package Pmp_Check_Config is + pragma Pure; + + Crate_Version : constant String := "0.1.0-dev"; + Crate_Name : constant String := "pmp_check"; + + Alire_Host_OS : constant String := "linux"; + + Alire_Host_Arch : constant String := "x86_64"; + + Alire_Host_Distro : constant String := "ubuntu"; + + type Build_Profile_Kind is (release, validation, development); + Build_Profile : constant Build_Profile_Kind := development; + +end Pmp_Check_Config; diff --git a/submissions/guillermovidalsule/config/pmp_check_config.gpr b/submissions/guillermovidalsule/config/pmp_check_config.gpr new file mode 100644 index 0000000..8aebe07 --- /dev/null +++ b/submissions/guillermovidalsule/config/pmp_check_config.gpr @@ -0,0 +1,50 @@ +-- Configuration for pmp_check generated by Alire +abstract project Pmp_Check_Config is + Crate_Version := "0.1.0-dev"; + Crate_Name := "pmp_check"; + + Alire_Host_OS := "linux"; + + Alire_Host_Arch := "x86_64"; + + Alire_Host_Distro := "ubuntu"; + Ada_Compiler_Switches := External_As_List ("ADAFLAGS", " "); + Ada_Compiler_Switches := Ada_Compiler_Switches & + ( + "-Og" -- Optimize for debug + ,"-ffunction-sections" -- Separate ELF section for each function + ,"-fdata-sections" -- Separate ELF section for each variable + ,"-g" -- Generate debug info + ,"-gnatwa" -- Enable all warnings + ,"-gnatw.X" -- Disable warnings for No_Exception_Propagation + ,"-gnatVa" -- All validity checks + ,"-gnaty3" -- Specify indentation level of 3 + ,"-gnatya" -- Check attribute casing + ,"-gnatyA" -- Use of array index numbers in array attributes + ,"-gnatyB" -- Check Boolean operators + ,"-gnatyb" -- Blanks not allowed at statement end + ,"-gnatyc" -- Check comments + ,"-gnaty-d" -- Disable check no DOS line terminators present + ,"-gnatye" -- Check end/exit labels + ,"-gnatyf" -- No form feeds or vertical tabs + ,"-gnatyh" -- No horizontal tabs + ,"-gnatyi" -- Check if-then layout + ,"-gnatyI" -- check mode IN keywords + ,"-gnatyk" -- Check keyword casing + ,"-gnatyl" -- Check layout + ,"-gnatym" -- Check maximum line length + ,"-gnatyn" -- Check casing of entities in Standard + ,"-gnatyO" -- Check that overriding subprograms are explicitly marked as such + ,"-gnatyp" -- Check pragma casing + ,"-gnatyr" -- Check identifier references casing + ,"-gnatyS" -- Check no statements after THEN/ELSE + ,"-gnatyt" -- Check token spacing + ,"-gnatyu" -- Check unnecessary blank lines + ,"-gnatyx" -- Check extra parentheses + ,"-gnatW8" -- UTF-8 encoding for wide characters + ); + + type Build_Profile_Kind is ("release", "validation", "development"); + Build_Profile : Build_Profile_Kind := "development"; + +end Pmp_Check_Config; diff --git a/submissions/guillermovidalsule/config/pmp_check_config.h b/submissions/guillermovidalsule/config/pmp_check_config.h new file mode 100644 index 0000000..2526d9b --- /dev/null +++ b/submissions/guillermovidalsule/config/pmp_check_config.h @@ -0,0 +1,20 @@ +/* Configuration for pmp_check generated by Alire */ +#ifndef PMP_CHECK_CONFIG_H +#define PMP_CHECK_CONFIG_H + +#define CRATE_VERSION "0.1.0-dev" +#define CRATE_NAME "pmp_check" + +#define ALIRE_HOST_OS "linux" + +#define ALIRE_HOST_ARCH "x86_64" + +#define ALIRE_HOST_DISTRO "ubuntu" + +#define BUILD_PROFILE_RELEASE 1 +#define BUILD_PROFILE_VALIDATION 2 +#define BUILD_PROFILE_DEVELOPMENT 3 + +#define BUILD_PROFILE 3 + +#endif diff --git a/submissions/guillermovidalsule/configuration.txt b/submissions/guillermovidalsule/configuration.txt new file mode 100644 index 0000000..aff16fd --- /dev/null +++ b/submissions/guillermovidalsule/configuration.txt @@ -0,0 +1,128 @@ +0x0F +0x08 +0x17 +0x1C +0x18 +0x99 +0x0 +0x0 +0x0 +0x0 +0x0 +0x0 +0x0 +0x0 +0x0 +0x0 +0x0 +0x0 +0x0 +0x0 +0x0 +0x0 +0x0 +0x0 +0x0 +0x0 +0x0 +0x0 +0x0 +0x0 +0x0 +0x0 +0x0 +0x0 +0x0 +0x0 +0x0 +0x0 +0x0 +0x0 +0x0 +0x0 +0x0 +0x0 +0x0 +0x0 +0x0 +0x0 +0x0 +0x0 +0x0 +0x0 +0x0 +0x0 +0x0 +0x0 +0x0 +0x0 +0x0 +0x0 +0x0 +0x0 +0x0 +0x0 +0x00001000 +0x00002000 +0x00003000 +0x0817ffff +0x00005000 +0x00006000 +0x00000000 +0x00000000 +0x00000000 +0x00000000 +0x00000000 +0x00000000 +0x00000000 +0x00000000 +0x00000000 +0x00000000 +0x00000000 +0x00000000 +0x00000000 +0x00000000 +0x00000000 +0x00000000 +0x00000000 +0x00000000 +0x00000000 +0x00000000 +0x00000000 +0x00000000 +0x00000000 +0x00000000 +0x00000000 +0x00000000 +0x00000000 +0x00000000 +0x00000000 +0x00000000 +0x00000000 +0x00000000 +0x00000000 +0x00000000 +0x00000000 +0x00000000 +0x00000000 +0x00000000 +0x00000000 +0x00000000 +0x00000000 +0x00000000 +0x00000000 +0x00000000 +0x00000000 +0x00000000 +0x00000000 +0x00000000 +0x00000000 +0x00000000 +0x00000000 +0x00000000 +0x00000000 +0x00000000 +0x00000000 +0x00000000 +0x00000000 +0x00000000 diff --git a/submissions/guillermovidalsule/pmp_check.gpr b/submissions/guillermovidalsule/pmp_check.gpr new file mode 100644 index 0000000..8fe7f95 --- /dev/null +++ b/submissions/guillermovidalsule/pmp_check.gpr @@ -0,0 +1,22 @@ +with "config/pmp_check_config.gpr"; +project Pmp_Check is + + for Source_Dirs use ("src/", "config/"); + for Object_Dir use "obj/" & Pmp_Check_Config.Build_Profile; + for Create_Missing_Dirs use "True"; + for Exec_Dir use "bin"; + for Main use ("pmp_check.adb"); + + package Compiler is + for Default_Switches ("Ada") use Pmp_Check_Config.Ada_Compiler_Switches; + end Compiler; + + package Binder is + for Switches ("Ada") use ("-Es"); -- Symbolic traceback + end Binder; + + package Install is + for Artifacts (".") use ("share"); + end Install; + +end Pmp_Check; diff --git a/submissions/guillermovidalsule/src/pmp.adb b/submissions/guillermovidalsule/src/pmp.adb new file mode 100644 index 0000000..af8d15d --- /dev/null +++ b/submissions/guillermovidalsule/src/pmp.adb @@ -0,0 +1,183 @@ + -------------------------------------------------------- + -- -- + -- Physical Memory Protection -- + -- -- + -- PMP.adb -- + -- -- + -- Copyright (C) 2025, G. V. S. -- + -- -- + -- Body -- + -- -- + -- This package implements the Physical Memory Prot- -- + -- ection (PMP) mechanism of the RISC-V architecture. -- + -- It is not meant for usage as part of a runtime, it -- + -- is based on the IDL verification coding challenge. -- + -- Also, please take into consideration that: -- + -- · There is no support for different granularities.-- + -- · (G)ranularity is always 0. NA4 is enabled. -- + -- · MPRV is not set. M always accesses as such. -- + -- · There is always one entry implemented minimum. -- + -- · This is the 64-bit version of this package. -- + -- · There are 64 PMP entries. -- + -- -- + -------------------------------------------------------- + +with Ada.Text_IO; + +package body Pmp is + + -- Verify whether an address is in range + function Verify_Address (Start_Address, + End_Address, + Arg_Address : Physical_Address) + return Boolean is + begin + return (Start_Address < End_Address) and then + (Start_Address <= Arg_Address) and then + (Arg_Address < End_Address); + end Verify_Address; + + -- Verify whether an operation is allowed + function Verify_Operation (Index : Pmp_Index; + Arg_Privilege_Mode : Privilege_Mode; + Arg_Operation : Operation) + return Boolean is + Access_Allowed : Boolean := False; + begin + -- If we are in M-Mode and L = 0 we can bypass + if Arg_Privilege_Mode = M and then pmpncfg (Index).L = 0 then + Access_Allowed := True; + else + case Arg_Operation is -- Is the operation permitted? + when R => + if pmpncfg (Index).R = 1 then + Access_Allowed := True; + end if; + when W => + if pmpncfg (Index).W = 1 then + Access_Allowed := True; + end if; + when X => + if pmpncfg (Index).X = 1 then + Access_Allowed := True; + end if; + end case; + end if; + return Access_Allowed; + end Verify_Operation; + + -- Prints whether an access is successfull or faults + procedure Print_Result (Result : Boolean) is + begin + if Result then + Ada.Text_IO.Put_Line ("Success"); + else + Ada.Text_IO.Put_Line ("Access Fault"); + end if; + end Print_Result; + + -- Set new granularity + procedure Set_Granularity (New_Granularity : Granularity) is + begin + G := New_Granularity; + end Set_Granularity; + + -- Add address to pmpaddr array at given Index + procedure Pmpaddr_Add_Address (New_Address : Pmp_Address; + Index : Pmp_Index) is + begin + pmpaddr (Index) := New_Address; + end Pmpaddr_Add_Address; + + -- Add entry to pmpcnfg array at given Index + procedure Pmpncfg_Add_Entry (New_Entry : Unsigned_8; + Index : Pmp_Index) is + begin + pmpncfg (Index).R := Integer (New_Entry and 1); + pmpncfg (Index).W := Integer (Shift_Right (New_Entry, 1) and 1); + pmpncfg (Index).X := Integer (Shift_Right (New_Entry, 2) and 1); + pmpncfg (Index).A := + Pmp_Mode'Val (Integer (Shift_Right (New_Entry, 3) and 3)); + pmpncfg (Index).Reserved := + Integer (Shift_Right (New_Entry, 5) and 3); + pmpncfg (Index).L := Integer (Shift_Right (New_Entry, 7) and 1); + end Pmpncfg_Add_Entry; + + -- Check whether an access is allowed with this PMP config + function Check_Access (Arg_Address : Physical_Address; + Arg_Privilege_Mode : Privilege_Mode; + Arg_Operation : Operation) + return Boolean is + begin + -- Find matching PMP entry + for Index in Pmp_Index'First .. Pmp_Index'Last loop + declare + Start_Address : Physical_Address; + End_Address : Physical_Address; + begin + -- Top of Range Mode + if pmpncfg (Index).A = TOR then + -- Set up range + if Index = Pmp_Index'First then + Start_Address := Physical_Address'First; + else + Start_Address := Shift_Left + (Physical_Address (pmpaddr (Index - 1)), 2); + end if; + End_Address := Shift_Left + (Physical_Address (pmpaddr (Index)), 2); + + -- Naturally-Aligned 4-byte region + elsif pmpncfg (Index).A = NA4 then + -- Set up range + Start_Address := Shift_Left + (Physical_Address (pmpaddr (Index)), 2); + End_Address := Start_Address + 4; + + -- Naturally-Aligned Power of Two Region + elsif pmpncfg (Index).A = NAPOT then + -- Set up range + declare + Shifted_Address : Pmp_Address := pmpaddr (Index); + Offset_Base_2 : Integer := 3; -- 2³ alignment + type Bit is mod 2; + LSB : Bit; + begin + loop -- Calculate address and size + LSB := Bit (Shifted_Address and 1); + exit when (LSB = 0) or else + (Offset_Base_2 = MSB); + Shifted_Address := Shift_Right (Shifted_Address, 1); + Offset_Base_2 := Offset_Base_2 + 1; + end loop; + Start_Address := Physical_Address (pmpaddr (Index) and + Shift_Left (Pmp_Address'Last, Offset_Base_2 - 3)); + Start_Address := Shift_Left (Start_Address, 2); + End_Address := Start_Address + 2 ** Offset_Base_2; + end; + + end if; + + -- Is address within range? + if pmpncfg (Index).A /= OFF and then + Verify_Address (Start_Address, End_Address, Arg_Address) + then + -- Check if operation is allowed + return Verify_Operation (Index, + Arg_Privilege_Mode, + Arg_Operation); + end if; + end; + + end loop; + -- 0 matches and we assume entries are implemented + -- so the access faults for S and U, but succeeds for M. + if Arg_Privilege_Mode = M then + return True; + else + return False; + end if; + + end Check_Access; + +end Pmp; diff --git a/submissions/guillermovidalsule/src/pmp.ads b/submissions/guillermovidalsule/src/pmp.ads new file mode 100644 index 0000000..59b8697 --- /dev/null +++ b/submissions/guillermovidalsule/src/pmp.ads @@ -0,0 +1,91 @@ + -------------------------------------------------------- + -- -- + -- Physical Memory Protection -- + -- -- + -- PMP.ads -- + -- -- + -- Copyright (C) 2025, G. V. S. -- + -- -- + -- Spec -- + -- -- + -- This package implements the Physical Memory Prot- -- + -- ection (PMP) mechanism of the RISC-V architecture. -- + -- It is not meant for usage as part of a runtime, it -- + -- is based on the IDL verification coding challenge. -- + -- Also, please take into consideration that: -- + -- · There is no support for different granularities.-- + -- · (G)ranularity is always 0. NA4 is enabled. -- + -- · MPRV is not set. M always accesses as such. -- + -- · There is always one entry implemented minimum. -- + -- · This is the 64-bit version of this package. -- + -- · There are 64 PMP entries. -- + -- -- + -------------------------------------------------------- + +with Interfaces; use Interfaces; + +package Pmp is + -- Types for Mode and Operation + type Privilege_Mode is (M, S, U); + type Operation is (R, W, X); + type Pmp_Mode is (OFF, TOR, NA4, NAPOT); + + -- Granularity + type Granularity is new Integer range 0 .. 0; + + -- Configuration architecture + type Architecture is (Riscv_32, Riscv_64); + + MSB : constant Integer := 55; + type Pmp_Address is new Unsigned_64 + range 0 .. 2**(MSB - 1) - 1; + type Physical_Address is new Unsigned_64 + range 0 .. 2**(MSB + 1) - 1; + + -- Array definitions for PMP entries and addresses + type Pmp_Index is range 0 .. 64 - 1; + type Pmpaddr_Array is array (Pmp_Index) of Pmp_Address; + type Pmp_Entry is record + L : Integer range 0 .. 1; -- Lock + Reserved : Integer range 0 .. 0; -- Reserved, 0 + A : Pmp_Mode; -- PMP mode + X : Integer range 0 .. 1; -- Execute + W : Integer range 0 .. 1; -- Write + R : Integer range 0 .. 1; -- Read + end record; + type Pmpncfg_Array is array (Pmp_Index) of Pmp_Entry; + + -- Arrays of PMP CSRs + pmpncfg : Pmpncfg_Array; + pmpaddr : Pmpaddr_Array; + + -- Functions, info on body + function Verify_Address (Start_Address, + End_Address, + Arg_Address : Physical_Address) + return Boolean; + + function Verify_Operation (Index : Pmp_Index; + Arg_Privilege_Mode : Privilege_Mode; + Arg_Operation : Operation) + return Boolean; + + procedure Print_Result (Result : Boolean); + procedure Set_Granularity (New_Granularity : Granularity); + + procedure Pmpaddr_Add_Address (New_Address : Pmp_Address; + Index : Pmp_Index); + + procedure Pmpncfg_Add_Entry (New_Entry : Unsigned_8; + Index : Pmp_Index); + + function Check_Access (Arg_Address : Physical_Address; + Arg_Privilege_Mode : Privilege_Mode; + Arg_Operation : Operation) + return Boolean; + +private + + G : Granularity := 0; + +end Pmp; diff --git a/submissions/guillermovidalsule/src/pmp_check.adb b/submissions/guillermovidalsule/src/pmp_check.adb new file mode 100644 index 0000000..d336d34 --- /dev/null +++ b/submissions/guillermovidalsule/src/pmp_check.adb @@ -0,0 +1,79 @@ +with Ada.Text_IO; +with Ada.Command_Line; +with Interfaces; use Interfaces; +with Pmp; use Pmp; + +procedure Pmp_Check is + package IO renames Ada.Text_IO; + package CL renames Ada.Command_Line; +begin + -- Check whether amount of Arguments is correct + if CL.Argument_Count /= 4 then + IO.Put_Line ("Usage"); + IO.New_Line; + IO.Put_Line (" ./pmp_check " & + " " & + " " & + " "); + IO.New_Line; + IO.Put_Line ("Where:"); + IO.Put_Line (" : Path to the configuration file"); + IO.Put_Line (" : Address in hexadecimal" & + " starting with 0x"); + IO.Put_Line (" : Either M, S or U"); + IO.Put_Line (" : Either (R)ead, (W)rite or" & + "e(X)ecute"); + return; + end if; + + declare + + -- Command Line Arguments + Arg_Path : constant String := CL.Argument (1); + Arg_Address : constant Physical_Address := + Physical_Address'Value ("16#" & + CL.Argument (2) (3 .. CL.Argument (2)'Last) & "#"); + Arg_Privilege_Mode : constant Privilege_Mode := + Privilege_Mode'Value (CL.Argument (3)); + Arg_Operation : constant Operation := + Operation'Value (CL.Argument (4)); + + -- File Related + F : IO.File_Type; + + begin + -- Open configuration file + IO.Open (F, IO.In_File, Arg_Path); + + -- Populate pmpncfg array with the input + for Index in Pmp.Pmp_Index'First .. Pmp.Pmp_Index'Last loop + declare + Line : constant String := IO.Get_Line (F); + Pmpn : constant Unsigned_8 := Unsigned_8'Value + ("16#" & Line (3 .. Line'Last) & "#"); + begin + Pmpncfg_Add_Entry (Pmpn, Index); + end; + end loop; + + -- Populate pmpaddr array with the input + for Index in Pmp_Index'First .. Pmp_Index'Last loop + declare + Line : constant String := IO.Get_Line (F); + Reg : constant Pmp_Address := Pmp_Address'Value + ("16#" & Line (3 .. Line'Last) & "#"); + begin + Pmpaddr_Add_Address (Reg, Index); + end; + end loop; + + -- Close stream + IO.Close (F); + + -- Check access + Print_Result (Check_Access (Arg_Address, + Arg_Privilege_Mode, + Arg_Operation)); + end; + +end Pmp_Check;