Data

Tools

Indexes

Applications

Experiments

Open Source Science

pipcore-mpu

https://github.com/2xs/pipcore-mpu

Science Score: 26.0%

This score indicates how likely this project is to be science-related based on various indicators:

  • ○
    CITATION.cff file
  • ✓
    codemeta.json file
    Found codemeta.json file
  • ✓
    .zenodo.json file
    Found .zenodo.json file
  • ○
    DOI references
  • ○
    Academic publication links
  • ○
    Academic email domains
  • ○
    Institutional organization owner
  • ○
    JOSS paper metadata
  • ○
    Scientific vocabulary similarity
    Low similarity (9.7%) to scientific vocabulary
Last synced: 10 months ago · JSON representation

Repository

Basic Info
  • Host: GitHub
  • Owner: 2xs
  • License: other
  • Language: Coq
  • Default Branch: master
  • Size: 18.1 MB
Statistics
  • Stars: 0
  • Watchers: 2
  • Forks: 0
  • Open Issues: 0
  • Releases: 0
Created over 3 years ago · Last pushed about 1 year ago
Metadata Files
Readme License Authors Codemeta

README.md

Readme

Pip-MPU is a project implementing the protokernel Pip on ARM Cortex-M devices having a Memory Protection Unit (MPU).

You can find more about the Pip protokernel at its website.

The source code is covered by CeCILL-A licence.

The Pip Development Team:

Past members of the Pip Development Team:

  • Quentin Bergougnoux

  • Julien Cartigny

  • Étienne Helluy Lafont

  • Narjes Jomaa

  • Paolo Torrini

  • Mahieddine Yaker

Repository structure

  • _CoqProject is a mandatory configuration file for Coq.

  • src contains the source base directory.

  • src/core contains the services code base.

  • src/extraction contains the code to extract Coq services.

  • src/interface contains the interface between Coq and C.

  • src/model contains the HAL Coq code.

  • src/arch/{architecture}/MAL contains the HAL C code.

  • src/arch/{architecture}/boot contains the "cbits", i.e the required C and assembly code required to boot the kernel.

  • tools contains the digger tool.

  • proof contains the Coq proof.

  • proof contains the documentation.

Dependencies

Pip-MPU is known to build correctly with this toolchain:

  • COQ Proof Assistant version 8.13.1

  • Doxygen version 1.9.3 and above (for documentation generation)

  • GCC version 12.1.0 and above

  • GNU Make version 4.3 and above

  • haskell-stack version 2.7.5 and above (is a cross-platform program for developing Haskell projects)

  • Texlive any version or another latex tools

Supported boards

Pip-MPU has been ported to:

  • DWM1001 (Nordic Semiconductors) - nRF52832 ARM Cortex-M4

Quick overview

Pip-MPU is specialised in memory isolation. It is based on a hierarchical TCB (Trusted Computing Base) made of nested partitions. Pip-MPU builds a partition tree where each children is isolated from each other.

Pip is originally based on the Memory Management Unit (MMU).

Pip-MPU retains Pip's philosophy and methodology adapted for constrained devices with a Memory Protection Unit (MPU), sorts of lightweigth MMU without memory virtualisation.

Pip-MPU is thus forked from the Pip original code base but completely revised to fit the MPU-empowered hardware platform.

More details on Pip-MPU can be read at Pip-MPU internals.

Benchmarks are provided in the 'benchmark' branch.

Pip-MPU services

Pip-MPU provides 15 system calls:

  • createPartition: creates a child partition

  • deletePartition: deletes a child partition

  • prepare: initialises a configuration block

  • collect: retrieves a configuration block

  • addMemoryBlock: adds a memory block to a child partition

  • removeMemoryBlock: removes a memory block from a child partition

  • cutMemoryBlock: cuts a memory block

  • mergeMemoryBlocks: merges back a memory block

  • mapMPU: activates a memory block in the real MPU

  • readMPU: reads which memory block is activates

  • findBlock: retrieves the memory block's attributes

  • setVIDT: sets the VIDT (Virtual Interrupt Descriptor Table) address of the current partition descriptor or of the partition descriptor of one of its children

  • yield: switches context

  • in: reads a register

  • out: writes a register

Getting started

Install the required packages to compile the documentation (for Ubuntu users):

console ~$ sudo apt install git make

Clone the repository: ```console

check the repository name is the same as this git repository

~$ git clone https://gitlab.univ-lille.fr/2xs/pip/pipcore-mpu.git ~$ cd pipcore-mpu ```

You can generate the "Getting Started" tutorial by invoking make gettingstarted. The full documentation is generated by invoking make doc.

Building options

You can pass several arguments to make to compile Pip-MPU.

  • all: Build target

  • proofs: Proofs target

  • doc | doc-c | doc-coq | gettingstarted: Documentation targets

  • clean | realclean: Clean targets

Funding

The pipcore-mpu project is part of the TinyPART project funded by the MESRI-BMBF German-French cybersecurity program under grant agreements n°ANR-20-CYAL-0005 and 16KIS1395K.

Owner

  • Name: 2XS
  • Login: 2xs
  • Kind: organization
  • Location: Université de Lille

CodeMeta (codemeta.json) 

{
  "@context": [
    "https://doi.org/10.5063/schema/codemeta-2.0"
  ],
  "@type": "SoftwareSourceCode",
  "name": "pipcore-mpu",
  "description": "Pip-MPU is a project implementing the protokernel Pip on ARM Cortex-M devices having a Memory Protection Unit (MPU).\r\n\r\nPip is a protokernel: it allows for kernels, ranging from hypervisors to monolithic kernels, to be developped as user mode applications. Pip only provides system calls for managing isolated partitions of the memory and basic dealing of control flow, thus reducing the trusted computing base to its bare minimum.\r\n\r\nThe logic of Pip is implemented in Gallina - the language of the Coq proof assistant - and it is in the process of being equipped with a formal proof that it ensures memory isolation. For efficiency, it is automatically translated into freestanding C code.\r\n\r\nThe architecture-dependent part of Pip is implemented in C and assembly language. It consists of a thin layer giving access to the hardware.",
  "dateCreated": "2021-02-03",
  "datePublished": "2024-01-31",
  "license": [
    "https://spdx.org/licenses/CECILL-2.1"
  ],
  "url": "https://hal.science/hal-04429589",
  "identifier": [],
  "applicationCategory": [
    "info"
  ],
  "keywords": [
    "Computer Science",
    "Provable Security",
    "Security",
    "Formal Methods",
    "Operating System",
    "Internet of Things",
    "IoT",
    "Embedded system"
  ],
  "funder": [
    {
      "@type": "Organization",
      "name": "MESRI"
    },
    {
      "@type": "Organization",
      "name": "BMBF"
    },
    {
      "@type": "Organization",
      "name": "ANR"
    }
  ],
  "codeRepository": "https://github.com/2xs/pipcore-mpu",
  "relatedLink": [
    "https://pip.univ-lille.fr/",
    "https://anr.fr/Projet-ANR-20-CYAL-0005",
    "https://github.com/2xs/pipcore",
    "https://github.com/2xs/dx",
    "https://github.com/2xs/digger"
  ],
  "programmingLanguage": [
    "Coq",
    "C",
    "Makefile",
    "Shell"
  ],
  "runtimePlatform": [
    "CoqIDE",
    "Coq"
  ],
  "version": "1",
  "softwareVersion": "1.0.0",
  "dateModified": "2024-01-31",
  "developmentStatus": "Actif",
  "referencePublication": {
    "hal": "hal-04185923,hal-03705114,tel-04093312,hal-03710419,hal-03679889,hal-03318078,hal-03102252,hal-03318088,hal-01819666"
  },
  "author": [
    {
      "@type": "Person",
      "givenName": "Damien",
      "familyName": "Amara",
      "affiliation": [
        {
          "@type": "Organization",
          "name": "Université de Lille"
        },
        {
          "@type": "Organization",
          "name": "CRIStAL"
        },
        {
          "@type": "Organization",
          "name": "2XS"
        }
      ]
    },
    {
      "@type": "Person",
      "givenName": "Quentin",
      "familyName": "Bergougnoux",
      "affiliation": [
        {
          "@type": "Organization",
          "name": "Université de Lille"
        },
        {
          "@type": "Organization",
          "name": "CRIStAL"
        },
        {
          "@type": "Organization",
          "name": "2XS"
        }
      ]
    },
    {
      "@type": "Person",
      "givenName": "Julien",
      "familyName": "Cartigny",
      "affiliation": [
        {
          "@type": "Organization",
          "name": "Université de Lille"
        },
        {
          "@type": "Organization",
          "name": "CRIStAL"
        },
        {
          "@type": "Organization",
          "name": "2XS"
        }
      ]
    },
    {
      "@type": "Person",
      "givenName": "Nicolas",
      "familyName": "Dejon",
      "affiliation": [
        {
          "@type": "Organization",
          "name": "Orange Labs Caen"
        },
        {
          "@type": "Organization",
          "name": "CRIStAL"
        },
        {
          "@type": "Organization",
          "name": "2XS"
        }
      ]
    },
    {
      "@type": "Person",
      "givenName": "Gilles",
      "familyName": "Grimaud",
      "affiliation": [
        {
          "@type": "Organization",
          "name": "Université de Lille"
        },
        {
          "@type": "Organization",
          "name": "CRIStAL"
        },
        {
          "@type": "Organization",
          "name": "2XS"
        }
      ]
    },
    {
      "@type": "Person",
      "givenName": "Michaël",
      "familyName": "Hauspie",
      "affiliation": [
        {
          "@type": "Organization",
          "name": "Université de Lille"
        },
        {
          "@type": "Organization",
          "name": "CRIStAL"
        },
        {
          "@type": "Organization",
          "name": "2XS"
        }
      ]
    },
    {
      "@type": "Person",
      "givenName": "Étienne",
      "familyName": "Helluy-Lafont",
      "affiliation": [
        {
          "@type": "Organization",
          "name": "CNRS"
        },
        {
          "@type": "Organization",
          "name": "CRIStAL"
        },
        {
          "@type": "Organization",
          "name": "2XS"
        }
      ]
    },
    {
      "@type": "Person",
      "givenName": "Samuel",
      "familyName": "Hym",
      "affiliation": [
        {
          "@type": "Organization",
          "name": "Université de Lille"
        },
        {
          "@type": "Organization",
          "name": "CRIStAL"
        },
        {
          "@type": "Organization",
          "name": "2XS"
        }
      ]
    },
    {
      "@type": "Person",
      "givenName": "Narjes",
      "familyName": "Jomaa",
      "affiliation": [
        {
          "@type": "Organization",
          "name": "Université de Lille"
        },
        {
          "@type": "Organization",
          "name": "CRIStAL"
        },
        {
          "@type": "Organization",
          "name": "2XS"
        }
      ]
    },
    {
      "@type": "Person",
      "givenName": "David",
      "familyName": "Nowak",
      "affiliation": [
        {
          "@type": "Organization",
          "name": "CNRS"
        },
        {
          "@type": "Organization",
          "name": "CRIStAL"
        },
        {
          "@type": "Organization",
          "name": "2XS"
        }
      ]
    },
    {
      "@type": "Person",
      "givenName": "Claire",
      "familyName": "Soyez-Martin",
      "affiliation": [
        {
          "@type": "Organization",
          "name": "Université de Lille"
        },
        {
          "@type": "Organization",
          "name": "CRIStAL"
        },
        {
          "@type": "Organization",
          "name": "2XS"
        }
      ]
    },
    {
      "@type": "Person",
      "givenName": "Paolo",
      "familyName": "Torrini",
      "affiliation": [
        {
          "@type": "Organization",
          "name": "Université de Lille"
        },
        {
          "@type": "Organization",
          "name": "CRIStAL"
        },
        {
          "@type": "Organization",
          "name": "2XS"
        }
      ]
    },
    {
      "@type": "Person",
      "givenName": "Florian",
      "familyName": "Vanhems",
      "affiliation": [
        {
          "@type": "Organization",
          "name": "Université de Lille"
        },
        {
          "@type": "Organization",
          "name": "CRIStAL"
        },
        {
          "@type": "Organization",
          "name": "2XS"
        }
      ]
    },
    {
      "@type": "Person",
      "givenName": "Mahieddine",
      "familyName": "Yaker",
      "affiliation": [
        {
          "@type": "Organization",
          "name": "Université de Lille"
        },
        {
          "@type": "Organization",
          "name": "CRIStAL"
        },
        {
          "@type": "Organization",
          "name": "2XS"
        }
      ]
    }
  ]
}

GitHub Events

Total
  • Push event: 20
  • Create event: 4
Last Year
  • Push event: 20
  • Create event: 4