Skip to content

Latest commit

 

History

History
185 lines (142 loc) · 7.88 KB

CHANGES.md

File metadata and controls

185 lines (142 loc) · 7.88 KB
Raw

Version history for capDL

Upcoming release

Changes

  • remove pyaml python dependency and use pyyaml (import yaml) directly.

Upgrade Notes

0.3 2024-07-01

Using seL4 version 13.0.0

Changes

  • add support for SMC capability
  • add support for binding notifications to TCBs
  • enable MCS build; use seL4_TCB_SetAffinity only for non-MCS kernels
  • allow SchedControlCap to refer to a secondary core
  • minimal update for seL4 AArch64 VSpace API change, removing seL4_ARM_PageGlobalDirectoryObject
  • object_sizes: add include for deprecated constants, because some definitions that object_sizes depends on are now found in a deprecated.h header file.
  • Clean up and clarify arm11 usage in capDL despite ARMv6 removal
  • cdl_utils: remove simpleeval python dependency
  • Run GitHub tests with python 3.9
  • added vulnerability reporting policy

capdl-loader

  • use seL4_BootInfoFrameSize instead of hard-coded page size
  • python + loader: Add support for generating fault handler caps with specific rights. Behaviour is unchanged (seL4_AllRights) if no rights are provided.
  • ensure heap is aligned

capDL-tool

  • update to LTS Haskell 20.25, ghc-9.2.8
  • fix several cases in validObjPars: Period, IOAPIC, MSIHandle, CBNumber

Upgrade Notes

  • existing capDL specs should continue to work
  • AArch64 VSpace changes may allow simplification of some capDL specs

0.2.1 2021-06-10

Using seL4 version 12.1.0

Changes

  • Added page-upper-directory caps to the valid TCB check for platforms like QEMU arm-virt as they use different paging structures.
  • Added const qualifiers to the capdl-loader-app to avoid compiler warnings against other libraries.
  • Improved the README for the capdl-loader-app.

Upgrade Notes

  • None to be aware of. This is not a source-breaking or binary-breaking release.

capdl-0.2.0 2020-10-27

Using seL4 version 12.0.0

Changes

  • Convert to SPDX license tags. This includes marking all documentation files CC-BY-SA-4.0.

  • Build system:

    • Support CMakeForegroundComplexCommands. This enables long-running build steps like Haskell installation to directly print to the console.
    • Make PLATFORM_SIFT agnostic of the build system directory layout
    • Save the binary artifacts for the capDL-tool in an out-of-build-tree directory, this will not rebuild in future if it can find a previously built artifact.
    • Migrate scripts to python3

  • Add seL4_BadgeBits constant and update python-capdl-tool to directly query the object_sizes dictionary. This allows for templates to use badge sizes.

  • Add support for Arm smmu v2.

  • Add support for Arm GetTrigger and GetTriggerCore seL4 invocations. This enables specs to correctly specify interrupt trigger mode and core affinities on Arm.

  • Add TCB Resume field to capDL object and support raw TCB object creation.

  • Add GitHub actions scripts. These scripts replicate internal CI checks directly on GitHub

capDL-tool

  • rework validObjCap and check TCB slots, which allows vcpus for all architectures.
  • convert CapDL language specification to Markdown.

Capdl-loader-app

  • Improve log output.
  • Initialise libc in debug builds.
  • Add check to only flush and invalidate kernel memory regions in capdl loader on Arm. Add platform_info header with memory window.
  • Add vcpu support for aarch64.
  • Handle IRQ binding to badged notifications properly: If an irq is bound to a notification with a non-zero badge, a badged capability is minted and used. Previously, the IRQ was bound to the unbadged notification.
  • Track number of used untypeds during object allocation and fail more gracefully if they run out.
  • Improve debugging printouts.
  • Fix issue where large DTB images inside BootInfo would overlap reserved memory address used to initialise frames.
  • Remove CONFIG_CAPDL_LOADER_ALLOW_NO_CSPACE config option as it has been unused for a while.

Capdl-linker

  • Optimize spec generation performance:
    • Sort elf symbols by their vaddr.
    • Replace linear search with binary when looking for virtual addresses.
  • Fix Python syntax warnings when capdl_linker.py is invoked.

0.1.0 2019-11-19

Using seL4 version 11.0.0

Changes

  • Add GrantReply access right for endpoint capabilities.
    • This is a new right available on seL4 Endpoint object capabilities.
    • A capDL spec can now describe an endpoint capability with the 'P' GrantReply access right.
    • The capdl-loader-app will create capabilities with these rights based on the translated spec.
    • python-capdl-tool supports creating endpoint caps with GrantReply rights.
  • Add object_sizes target.
    • This target generates a YAML file describing the object size of each seL4 object.
    • It is based on the current build configuration of the kernel.
    • This file can be used as an input to tools performing allocation of seL4 objects from untypeds.
  • Add untyped_gen.py in cdl_utils.
    • This is only supported on Arm architectures currently.
    • This tool generates a predicted list of untypeds that the kernel will provide to userlevel
    • This list is calculated from an input of memory regions for the platform and sizes of the kernel image and device tree binary.
    • The list is intended to be used as an input for an allocator to perform allocation of initial system resources.
  • capDL untyped allocation
    • Add support for generating a capDL spec that specifies which untyped object each object and capability is allocated from. This is intended to be used when implementing trustworthy system initialisers as it removes online allocation decisions and results in a simpler init program.
    • This is only supported on Arm.
  • Static allocator
    • Updates capdl-loader-app to load static specs with all objects allocated from a predicted list of untypeds.
    • This simpler version of the loader app will act as a reference implementation for a more trustworthy implementation that is in development.
    • This is only supported on Arm.
  • RISC-V support added
    • Support for generating, translating and loading RISC-V applications.
  • seL4runtime updates
    • Port capdl-loader-app to sel4runtime
  • cdl-refine
    • This support is closely tied to CAmkES and L4V.
    • The capDL-tool can translate specs into Isabelle .thy file formats. These are then used to calculate which access rights different parts of the system have to each other.
    • It is used to check that the capDL system spec implements certain access policies as specified by an external source.
    • See cdl-refine in the context of CAmkES for more information.
  • 40-bit PA for aarch64 hyp
    • When seL4 is running in EL2 on aarch64, VSpace objects are an abstraction of stage 2 translations. These translations have different input address restrictions based on the physical address range the CPU supports. 40-bit PA support supports platforms that have 40-bit stage 2 input address ranges when in hyp-mode.
  • Remove --code-max-irqs from capDL tool
    • The capDL-tool that translates capDL formats no longer requires --code-max-irqs as an option for generating C specs. It now infers the total IRQs from the input spec and specifies this value in the generated C spec.
  • Add FrameFill mechanism for files and use this to implement ELF loading
    • The FrameFill mechanism allows Frame objects to be annotated with an attribute describing a way to initialise their contents by a loader.
    • The new file FrameFill mechanism allows frames to be initialised from the contents of a file provided to the loader in a cpio archive.
    • This mechanism is used to remove ELF loader support from the initialiser. Instead a spec describes how frames are initialised via copies from offsets into a provided ELF file.
    • This allows a loader to load program data from different file formats also.