--- title: AWS proves its hypervisor safe on paper, FreeBSD lets... description: AWS shipped a formally verified isolation engine for its newest EC2 instances, backed by 330,000 lines of machine-checked proofs. Meanwhile a real FreeBSD... canonical: https://daily.dev/posts/aws-proves-its-hypervisor-safe-on-paper-freebsd-lets-any-user-write-to-root-hq0icrwu9 twitter:card: summary_large_image twitter:site: @dailydotdev og:type: website og:site_name: daily.dev og:title: AWS proves its hypervisor safe on paper, FreeBSD lets any user write to root | daily.dev og:description: AWS shipped a formally verified isolation engine for its newest EC2 instances, backed by 330,000 lines of machine-checked proofs. Meanwhile a real FreeBSD... og:url: https://daily.dev/posts/aws-proves-its-hypervisor-safe-on-paper-freebsd-lets-any-user-write-to-root-hq0icrwu9 og:image: https://api.daily.dev/og/posts/HQ0IcRwU9.png og:image:alt: AWS proves its hypervisor safe on paper, FreeBSD lets any user write to root og:image:width: 1200 og:image:height: 630 og:locale: en --- > ## Documentation Index > Fetch the complete documentation index at: https://daily.dev/llms.txt > Use this file to discover all available pages before exploring further. # AWS proves its hypervisor safe on paper, FreeBSD lets any user write to root **[Security Digest](https://daily.dev/sources/security_digest)** · 4 min read · 0 upvotes · 0 comments ## Summary AWS shipped a formally verified isolation engine for its newest EC2 instances, backed by 330,000 lines of machine-checked proofs. Meanwhile a real FreeBSD kernel bug lets any local user escalate to root by chaining sendfile, kTLS, and SUID corruption. A ProjectDiscovery audit found five chained CVEs in a VS Code extension with 9.5 million installs, and a new macOS stealer clones live browser sessions instead of just stealing cookies. Also today: a researcher's breakdown of why Supabase apps without proper auth wiring end up with exposed databases by default. ## Content **TLDR:** AWS shipped a formally verified isolation engine for its newest EC2 instances, backed by 330,000 lines of machine-checked proofs. Meanwhile a real FreeBSD kernel bug lets any local user escalate to root by chaining sendfile, kTLS, and SUID corruption. A ProjectDiscovery audit found five chained CVEs in a VS Code extension with 9.5 million installs, and a new macOS stealer clones live browser sessions instead of just stealing cookies. Also today: a researcher's breakdown of why Supabase apps without proper auth wiring end up with exposed databases by default. --- ## AWS's new Nitro Isolation Engine is a formally verified hypervisor, not just a marketing claim The Graviton5-powered M9g and M9gd EC2 instances run on a separation kernel written in a restricted Rust subset called μRust, with VM isolation proven mathematically using the Isabelle/HOL proof assistant. AWS produced 330,000 lines of machine-checked proofs covering confidentiality, integrity, and memory safety, and open-sourced the underlying AutoCorrode proof infrastructure last year. This is the first formally verified hypervisor running in a commercial cloud, in the same league as the seL4 project people have cited for over a decade as the gold standard. [Read more](https://daily.dev/posts/xonDXKppx) ## CVE-2026-45257: unprivileged FreeBSD users can write to any file and pivot to root By chaining sendfile's vnode-backed EXTPG mbufs, the unprivileged TCP_RXTLS_ENABLE socket option, and in-place AES-GCM decryption through PHYS_TO_DMAP, any local user can write attacker-chosen bytes into a file's page cache. That bypasses chflags schg and VFS permission checks entirely, and corrupting a SUID binary like /usr/bin/su turns it into root. It hits FreeBSD 13.0 through 15.0 on amd64/arm64/riscv with the default kern.ipc.mb_use_ext_pgs=1 setting, a patch has already shipped, and setting mb_use_ext_pgs=0 works as a stopgap. [Read more](https://daily.dev/posts/QCQRau2Dy) ## Five chained CVEs found in a VS Code extension with 9.5 million installs ProjectDiscovery's Neo agent audited Markdown Preview Enhanced and found a WaveDrom diagram block that triggers eval() inside the preview webview, chaining through an unvalidated postMessage dispatcher to arbitrary file write on disk (CVE-2026-50733). Further digging turned up a VM sandbox escape giving OS command execution, stored XSS via head.html injection, and two shared infrastructure flaws in the command dispatcher. All five are fixed in v0.8.28 through v0.8.30, with eval replaced by JSON parsing and the VM sandbox swapped for a WASM-isolated QuickJS engine — update now if you have this installed. [Read more](https://daily.dev/posts/Mj5pPG0hr) ## AmnesiaStealer clones live authenticated browser sessions on macOS, not just cookies Spread via ClickFix campaigns using fake GitHub download pages, AmnesiaStealer clones a victim's Chromium profile and loads it into a hidden headless browser attackers can control live over the Chrome DevTools Protocol, complete with mouse/keyboard input and a screencast. It targets 16 Chromium browsers plus keychain data, Apple Notes, Telegram sessions, and crypto wallets, and on macOS 26 it corrupts the Chrome Safe Storage key when it can't recover it, permanently breaking stored credentials while the attacker keeps access. Jamf calls it the first documented macOS malware combining cloned Chromium profiles with live CDP remote control. [Read more](https://daily.dev/posts/nPTpus9uC) --- ## Also notable - **Supabase apps without proper auth wiring hit 35.8% critical vulnerability rates:** An analysis of 1,236 AI-built apps found that pairing Supabase with a third-party auth library pushes critical findings to 35.8%, versus 4.2% for apps without Supabase at all, because the auth library never issues the token Supabase's row-level security checks against. [Read more](https://daily.dev/posts/w6mw2xewx) - **Trump memo lets vetted US companies conduct offensive cyber operations for the government:** The new National Security Presidential Memorandum requires participating companies to hold at least a $1 million bond or escrow while conducting government-directed surveillance and offensive cyber actions against foreign adversaries. [Read more](https://daily.dev/posts/vIyMVUrjd) - **SafePal breach exposes 39,798 customers via an order-tracking plug-in flaw:** Names, emails, addresses, and purchase history for buyers between March 2025 and April 2026 are now for sale on a cybercrime forum, though seed phrases and payment data weren't exposed. [Read more](https://daily.dev/posts/dZgepJwHn) - **Kimsuky is building local LLM infrastructure for AI-assisted attacks, not training its own models:** Genians found the North Korea-linked group running Ollama, GPT4All, and RAG pipelines alongside AsyncRAT payloads in Operation GitPower, putting it in a capability-building phase rather than active model training. [Read more](https://daily.dev/posts/rDMlMe7Aw) - **AWS open-sources Dogwood to let Cedar policies reason about sequences of agent tool calls:** The extension adds temporal operators like count_within and sum_within for rate limits and running totals across an agent's prior actions, but AWS is explicit that the reference interpreter is not production-ready. [Read more](https://daily.dev/posts/BXI8dF9Jv) ## Similar posts on daily.dev - [CVE-2026-45257: LPE in FreeBSD via kTLS-RX](https://daily.dev/posts/cve-2026-45257-lpe-in-freebsd-via-ktls-rx-qcqrau2dy) · Lobsters · 0 upvotes · 0 comments - [This Week In Security: Microsoft On Microsoft, Register Your Domains, Linux On ARM, And FreeBSD Joins The File Cache Club](https://daily.dev/posts/this-week-in-security-microsoft-on-microsoft-register-your-domains-linux-on-arm-and-freebsd-join-7v9zowz3e) · Hackaday · 0 upvotes · 0 comments --- Tags: [#security](https://daily.dev/tags/security), [#aws](https://daily.dev/tags/aws), [#linux](https://daily.dev/tags/linux), [#vscode](https://daily.dev/tags/vscode) [View this post on daily.dev](https://daily.dev/posts/aws-proves-its-hypervisor-safe-on-paper-freebsd-lets-any-user-write-to-root-hq0icrwu9) ```json {"@context":"https://schema.org","@graph":[{"@type":"Organization","@id":"https://daily.dev/#organization","name":"daily.dev","url":"https://daily.dev","logo":{"@type":"ImageObject","url":"https://daily.dev/apple-touch-icon.png","width":180,"height":180},"sameAs":["https://twitter.com/dailydotdev","https://github.com/dailydotdev","https://www.linkedin.com/company/daily-dev-ltd"]},{"@type":"WebSite","@id":"https://daily.dev/#website","url":"https://daily.dev","name":"daily.dev","publisher":{"@id":"https://daily.dev/#organization"},"potentialAction":{"@type":"SearchAction","target":{"@type":"EntryPoint","urlTemplate":"https://daily.dev/search?q={search_term_string}"},"query-input":"required name=search_term_string"}}]} {"@context":"https://schema.org","@type":"DiscussionForumPosting","mainEntityOfPage":"https://daily.dev/posts/aws-proves-its-hypervisor-safe-on-paper-freebsd-lets-any-user-write-to-root-hq0icrwu9","headline":"AWS proves its hypervisor safe on paper, FreeBSD lets any user write to root","text":"AWS shipped a formally verified isolation engine for its newest EC2 instances, backed by 330,000 lines of machine-checked proofs. Meanwhile a real FreeBSD kernel bug lets any local user escalate to root by chaining sendfile, kTLS, and SUID corruption. A ProjectDiscovery audit found five chained CVEs in a VS Code extension with 9.5 million installs, and a new macOS stealer clones live browser sessions instead of just stealing cookies. Also today: a researcher's breakdown of why Supabase apps without proper auth wiring end up with exposed databases by default.","url":"https://daily.dev/posts/aws-proves-its-hypervisor-safe-on-paper-freebsd-lets-any-user-write-to-root-hq0icrwu9","datePublished":"2026-08-17T04:18:06.243Z","dateModified":"2026-08-17T04:18:31.396Z","author":{"@type":"Organization","name":"Security Digest","logo":"https://media.daily.dev/image/upload/s--m4ZKB_C0--/f_auto,q_auto/v1779959612/logos/security_digest","url":"https://daily.dev/sources/security_digest"},"interactionStatistic":[{"@type":"InteractionCounter","interactionType":{"@type":"LikeAction"},"userInteractionCount":0},{"@type":"InteractionCounter","interactionType":{"@type":"CommentAction"},"userInteractionCount":0}],"isPartOf":{"@type":"WebPage","url":"https://daily.dev/sources/security_digest","name":"Security Digest"}} {"@context":"https://schema.org","@type":"BreadcrumbList","itemListElement":[{"@type":"ListItem","position":1,"name":"Home","item":"https://daily.dev"},{"@type":"ListItem","position":2,"name":"Security Digest","item":"https://daily.dev/sources/security_digest"},{"@type":"ListItem","position":3,"name":"AWS proves its hypervisor safe on paper, FreeBSD lets any user write to root"}]} ```