Our great sponsors
seL4 | rekor | |
---|---|---|
59 | 29 | |
4,492 | 828 | |
1.2% | 2.4% | |
9.0 | 9.7 | |
7 days ago | 10 days ago | |
C | Go | |
GNU General Public License v3.0 or later | Apache License 2.0 |
Stars - the number of stars that a project has on GitHub. Growth - month over month growth in stars.
Activity is a relative number indicating how actively a project is being developed. Recent commits have higher weight than older ones.
For example, an activity of 9.0 indicates that a project is amongst the top 10% of the most actively developed projects that we are tracking.
seL4
-
On the Costs of Syscalls
There are also RTOS-capable microkernels such as seL4[0], with few but extremely fast syscalls[1]. Note times are in cycles, not usec.
-
Can the language of proof assistants be used for general purpose programming?
https://sel4.systems
Working on a number of platforms, verified on some. Multicore support is an ongoing effort afaict.
On OS built on this kernel is still subject to some assumptions (like, hardware working correctly, bootloader doing its job, etc). But mostly those assumptions are less of a problem / easier to prove than the properties of a complex software system.
As I understand it, guarantees that seL4 does provide, go well beyond anything else currently out there.
-
Basic SAT model of x86 instructions using Z3, autogenerated from Intel docs
You can use it to (mostly) validate small snippets are the same. See Alive2 for the application of Z3/formalization of programs as SMT for that [1]. As far as I'm aware there are some problems scaling up to arbitrarily sized programs due to a lack of formalization in higher level languages in addition to computational constraints. With a lot of time and effort it can be done though [2].
-
What are the current hot topics in type theory and static analysis?
Formal methods. This is not in most general-purpose programming languages and probably never will be (maybe we'll see formal methods to verify unsafe code in Rust...) because it's a ton of boilerplate (you have to help the compiler type-check your code) and also extremely complicated. However, formal methods is very important for proving code secure, such as sel4 (microkernel formally verified to not have bugs or be exploitable) which has just received the ACM Software Systems Award 3 days ago.
- Rust Now Available for Real-Time Operating System and Hypervisor PikeOS
-
A plan for cybersecurity and grid safety
Efforts: seL4, Project Everest, the Prossimo project of the ISRG, Let's Encrypt, and Prusti for the Rust language
- Better not fire anyone now
-
Linux Kernel Ksmbd Use-After-Free Remote Code Execution Vulnerability
Yet another exploit that just wouldn't be possible on a well-designed system, such as Genode[0] with seL4[1].
Monolithic UNIX clones are an anachronism we should get rid of.
-
Pegasus spyware was used to hack reporters’ phones. I’m suing its creators; When you’re infected by Pegasus, spies effectively hold a clone of your phone – we’re fighting back.
There is also a long-term idea with Qubes OS of supporting seL4 as a secure kernel (although there are issues to fix first, some of which also make it clear just why seL4 sees few mention as far as desktops go right now - these are the practical issues I was mentioning).
The reliance on Linux's kernel (rather than something more secure) and its networking stack (implemented in C without formal verification, like the rest of the kernel), also means that the odd exploitable network bug can remain exploitable forever because of the fucked up Android ecosystem which usually leads to manufacturers dropping updates fairly soon after the release of a phone.
rekor
-
Obtainium – Get Android App Updates Directly from the Source
There could be asset hashes in sigstore: https://sigstore.dev/
Is there a good way to run native mobile app GUI tests with GitHub Actions?
A VM/container emulator like anbox, waydroid, (or all of ChromeOS Flex in KVM) in a GitHub Action is probably enough to run GUI tests?
"Build your own SLSA 3+ provenance builder on GitHub Actions"
- Why SQLite Does Not Use Git
-
An Overview of Kubernetes Security Projects at KubeCon Europe 2023
sigstore is another suite of tools that focuses on attestation and provenance. Within the suite are two tools I heard mentioned a few times at KubeCon: Cosign and Rekor.
- 50% new NPM packages are spam
-
Spin 1.0 — The Developer Tool for Serverless WebAssembly
Since we can distribute Spin applications using popular registry services, we can also take advantage of ecosystem tools such as Sigstore and Cosign, which address the software supply chain issue by signing and verifying applications using Sigstore's new keyless signatures (using OIDC identity tokens from providers such as GitHub).
-
Build and sign application containers
With containers being the heart of Cloud Native application development, it has become even more critical to ensure the integrity of the containers. One of the ways to do this to sign and verify the container images.sigstore is a open source project that empowers software developers to securely sign the container images.
-
Ask HN: What is the most impactful thing you've ever built?
https://sigstore.dev - although its really not true to say I built it. I started it off, but very quickly smarter folks then me jumped on board and really took it to all sorts of new directions.
-
Container Images for the Cloud Native Era
Powered by Wolfi, Chainguard Images are a suite of distroless images that consolidate the base features of the Wolfi undistro into end-user container images that can be integrated into existing workflows. Chainguard Images are fully declarative and reproducible, and include SBOMs that cover all image dependencies. In addition, Chainguard Images are signed via Sigstore, which attests the provenance of all artifacts. All images and corresponding signatures, as well as their SBOMs, are hosted in Chainguard's OCI registry cgr.dev.
-
I am Mikko Hypponen, a global infosec expert! Ask me anything.
What's your thoughts on the sigstore project from the linux foundation?
-
Freezing Requirements with Pip-Tools
https://docs.sigstore.dev/ :
> sigstore empowers software developers to securely sign software artifacts such as release files, container images, binaries, bill of material manifests and more. Signing materials are then stored in a tamper-resistant public log.
> It’s free to use for all developers and software providers, with sigstore’s code and operational tooling being 100% open source, and everything maintained and developed by the sigstore community.
> How sigstore works: Using Fulcio, sigstore requests a certificate from our root Certificate Authority (CA). This checks you are who you say you are using OpenID Connect, which looks at your email address to prove you’re the author. Fulcio grants a time-stamped certificate, a way to say you’re signed in and that it’s you.
https://github.com/sigstore/fulcio
> You don’t have to do anything with keys yourself, and sigstore never obtains your private key. The public key that Cosign creates gets bound to your certificate, and the signing details get stored in sigstore’s trust root, the deeper layer of keys and trustees and what we use to check authenticity.
https://github.com/sigstore/cosign
> our certificate then comes back to sigstore, where sigstore exchanges keys, asserts your identity and signs everything off. The signature contains the hash itself, public key, signature content and the time stamp. This all gets uploaded to a Rekor transparency log, so anyone can check that what you’ve put out there went through all the checks needed to be authentic.
What are some alternatives?
sigstore-the-hard-way - sigstore the hard way!
fulcio - Sigstore OIDC PKI
l4v - seL4 specification and proofs
fprime - F´ - A flight software and embedded systems framework
cosign - Code signing and transparency for containers and binaries
nomicon - The Dark Arts of Advanced and Unsafe Rust Programming
CompCert - The CompCert formally-verified C compiler
InitWare - The InitWare Suite of Middleware allows you to manage services and system resources as logical entities called units. Its main component is a service management ("init") system.
4.4BSD-Lite2 - 4.4BSD Lite Release 2: last Unix operating system from Berkeley
kubeclarity - KubeClarity is a tool for detection and management of Software Bill Of Materials (SBOM) and vulnerabilities of container images and filesystems
Covenant - Covenant is a collaborative .NET C2 framework for red teamers.
openc910 - OpenXuantie - OpenC910 Core