Google Announces KataOS and Sparrow

This page summarizes the projects mentioned and recommended in the original post on news.ycombinator.com

InfluxDB - Power Real-Time Data Analytics at Scale
Get real-time insights from all types of time series data with InfluxDB. Ingest, query, and analyze billions of data points in real-time with unbounded cardinality.
www.influxdata.com
featured
SaaSHub - Software Alternatives and Reviews
SaaSHub helps you find the best software and product alternatives
www.saashub.com
featured
  • sparrow-kernel

    Discontinued The seL4 microkernel

  • Yes, especially 'logically impossible' when you dig into the details. From the blogpost:

    > and the kernel modifications to seL4 that can reclaim the memory used by the rootserver.

    MMMMMMMMMMMkkkkkk. So you then have to ask: were these changes also formally verified? There's a metric ton of kernel changes here: https://github.com/AmbiML/sparrow-kernel/commits/sparrow but I don't see a fork of https://github.com/seL4/l4v anywhere inside AmbiML.

    I mean, it does also claim to be "almost entirely written in Rust", which is true if you ignore almost the entire OS part of the OS (the kernel and the minimal seL4 runtime).

  • l4v

    seL4 specification and proofs

  • Yes, especially 'logically impossible' when you dig into the details. From the blogpost:

    > and the kernel modifications to seL4 that can reclaim the memory used by the rootserver.

    MMMMMMMMMMMkkkkkk. So you then have to ask: were these changes also formally verified? There's a metric ton of kernel changes here: https://github.com/AmbiML/sparrow-kernel/commits/sparrow but I don't see a fork of https://github.com/seL4/l4v anywhere inside AmbiML.

    I mean, it does also claim to be "almost entirely written in Rust", which is true if you ignore almost the entire OS part of the OS (the kernel and the minimal seL4 runtime).

  • InfluxDB

    Power Real-Time Data Analytics at Scale. Get real-time insights from all types of time series data with InfluxDB. Ingest, query, and analyze billions of data points in real-time with unbounded cardinality.

    InfluxDB logo
  • camkes-tool

    The main CAmkES tool

  • Those names come from the existing seL4 project that these googlers are merely using/forking.

    (CAmkES is a hot mess, and "unpleasantly too much C" if you ask me. https://docs.sel4.systems/projects/camkes/ & https://github.com/seL4/camkes-tool/blob/master/docs/index.m...)

NOTE: The number of mentions on this list indicates mentions on common posts plus user suggested alternatives. Hence, a higher number means a more popular project.

Suggest a related project

Related posts

  • SeL4 Specification and Proofs

    1 project | news.ycombinator.com | 20 Aug 2023
  • Proofs and specifications

    1 project | /r/RISCV | 13 Mar 2022
  • Proofs and specifications

    1 project | /r/kernel | 13 Mar 2022
  • Proofs and specifications

    1 project | /r/computerscience | 13 Mar 2022
  • Proofs and specifications

    1 project | /r/seL4 | 13 Mar 2022