Opening Keynote

A Better Science and Engineering of Security: Lessons from Apple's Leading Edge

Speakers: Ivan Krstić, Head of Security Engineering and Architecture, Apple

Conference: Hexacon

YouTube: https://www.youtube.com/watch?v=Du8BbJg2Pj4

Overview

In this Hexacon keynote, Ivan Krstić, Head of Security Engineering and Architecture at Apple, presented a compelling vision for the future of security, arguing that the field is experiencing an unprecedented velocity of progress driven by a more scientific approach integrated with robust engineering. Krstić emphasized that at the leading edge, security is already remarkably strong, a testament to the maturation of both security science, which defines rigorous models and verifies correctness, and security engineering, which constructs secure systems under severe real-world constraints. A central theme was the pivotal role of deeply integrating offensive research into the defense engineering loop, catalyzed by advanced tooling.

Krstić illustrated this evolution through three distinct case studies from Apple's security initiatives: the formal verification of Core Crypto for quantum-resistant algorithms, the architectural overhaul of page table management with the Secure Page Table Monitor (SPTM), and the ambitious Memory Integrity Engine (MIE) designed to neutralize memory safety bugs. Beyond these technical deep dives, the talk also unveiled significant updates to the Apple Security Bounty program, including dramatically increased rewards and innovative verification methods, and concluded with a powerful call to action for security researchers to consider the ethical implications and societal impact of their work.

This address underscores Apple's commitment to pushing the boundaries of platform security, not merely through incremental fixes but through foundational architectural changes, rigorous scientific validation, and a proactive engagement with offensive security expertise. It provides a blueprint for how large-scale, complex systems can achieve higher levels of assurance, demonstrating that the pursuit of a "better science and engineering of security" is not just an aspiration but an achievable reality with profound implications for user protection.

Background

▶ Watch: Introduction to better science and engineering of security (0:00)

The journey towards a more scientific and robust approach to security is born from the persistent challenges faced by traditional security engineering. Historically, many critical security components, particularly in cryptography and operating system kernels, have evolved through iterative fixes and a reliance on expert intuition rather than formal proofs or architectural guarantees. This has led to recurring vulnerabilities, design flaws, and a reactive security posture.

For instance, in the realm of cryptography, the TLS 1.3 protocol emerged following a "long embarrassing series of vulnerabilities" in earlier TLS versions, such as Beast, Crime, and Poodle. These incidents highlighted the limitations of even widely reviewed cryptographic protocols when formal methods were not rigorously applied to their design and implementation. Similarly, within operating system kernels, the complexity of components like page table managers often creates an expansive Trusted Computing Base (TCB) with poorly understood boundaries. Apple's prior Page Protection Layer (PPL), while conceptually sound, suffered from practical implementation challenges, allowing an attacker with a kernel read/write primitive to directly manipulate page tables and execute arbitrary unsigned code. This demonstrated how even well-intentioned security features could be undermined by subtle bugs in virtual address handling, ubiquitous and often incorrect pointer math, and loosely permitted invalid state transitions.

The pervasive issue of memory safety bugs across software development also forms a critical part of this background. Traditional memory allocators often exhibit predictable behaviors that attackers can leverage to reliably achieve exploitation, allowing for generic and reusable exploit primitives. The lack of precise models for memory corruption and the sheer volume of code make traditional auditing and patching an insufficient defense against these fundamental vulnerabilities. These systemic issues underscored the need for a paradigm shift—moving beyond solely engineering what can be built, to scientifically determining what should be built and rigorously verifying its correctness. This shift requires not only advanced technical solutions but also a fundamental re-evaluation of development processes, tooling, and the integration of diverse security expertise, including offensive research, from the earliest stages of design.

Key Findings

▶ Watch: First story: Core Crypto and quantum-safe algorithms (1:51)

Krstić's talk highlighted several key findings and advancements across Apple's security landscape, demonstrating the tangible benefits of integrating scientific rigor with engineering excellence and offensive research.

Firstly, in Core Crypto, Apple successfully achieved high assurance for new quantum-resistant algorithms like MLCAM and MLDDSA. This was accomplished by combining formal methods with custom-built tooling capable of verifying highly optimized assembly implementations against high-level mathematical specifications. This approach ensures cryptographic correctness even for novel, less-understood algorithms and hand-tuned performance-critical code.

Secondly, the introduction of the Secure Page Table Monitor (SPTM) as a replacement for the older PPL represents a significant architectural leap. By designing SPTM as a clean, least-privilege architecture logically and architecturally distinct from XNU (Apple's kernel), Apple was able to architecturally prevent 95% of the known issues that plagued the PPL. This proactive design, coupled with formal verification of its state machine and deep offensive team engagement, has resulted in a system that has never been successfully exploited in the wild or through Apple's bounty program, a finding corroborated by a six-month independent audit.

Thirdly, the Memory Integrity Engine (MIE) stands out as a monumental effort to fundamentally alter the memory corruption exploitation landscape. MIE aims to render most memory safety bugs unexploitable and force any remaining ones to require completely custom, non-reusable exploitation strategies. Through a precise memory corruption model, type-aware sequestering, allocation fronts, enhanced MTE, and novel Spectre v1 mitigation, MIE has proven to deterministically break real-world exploit chains. The extensive offensive evaluation, including researching novel MIE-resistant techniques before launch, provided Apple with a multi-year head start in countering emerging threats.

Finally, beyond technical advancements, Apple's commitment to fostering external security research was underscored by a significant update to the Apple Security Bounty program. Rewards for top categories were substantially increased, with zero-click attacks now offering up to $2 million (and a theoretical maximum exceeding $5 million with bonuses). The introduction of target flags provides a transparent and expedited mechanism for researchers to demonstrate their capabilities and receive prompt payouts, adapting the program to the increasing difficulty of exploiting Apple platforms. These combined findings paint a picture of a security ecosystem where proactive design, rigorous verification, and collaborative offensive/defensive efforts yield robust, real-world protections.

Technical Deep Dive

▶ Watch: New custom tool for assembly verification in Core Crypto (4:40)

The core of Apple's advanced security initiatives lies in the detailed technical implementations across its critical components. Krstić elaborated on three distinct projects: Core Crypto, SPTM, and MIE, each showcasing a blend of scientific modeling, rigorous engineering, and offensive security integration.

Core Crypto: Formal Verification for Quantum-Resistant Algorithms

The challenge in Core Crypto arose with the integration of new lattice-based algorithms like MLCAM and MLDDSA, which are designed to be secure against future quantum attacks. Unlike traditional elliptic curve cryptography, these new constructions are susceptible to "silent implementation failures," and the cryptographic community has less experience with their practical deployment. To achieve maximum high assurance, Apple turned to formal methods and computer-assisted proof tools.

The process involves several steps:

1. High-Level Specification: Translating the cryptographic standard into a high-level mathematical specification.
2. Code to Low-Level Specification: Using tools like Saw and Cryptol to map the C code implementation to a low-level mathematical pseudocode specification. This step can be performed by skilled cryptographic developers without deep formal methods expertise.
3. Mathematical Equivalence Proofs: Employing tools like Isabel to prove mathematical equivalences between the high-level specification and the low-level specification derived from the C code.
4. Assembly Verification (Custom Tool): A critical and unique step. Since Apple uses highly optimized, hand-tuned assembly implementations for performance and battery efficiency—which existing formal tools cannot directly parse—a completely new custom tool was developed. This tool proves the equivalence of the assembly functions to their verified C implementations.

This end-to-end verification covers the entire implementation stack, from the standard to the C code to the assembly. Importantly, it also verifies properties like memory safety and the absence of undefined behavior, providing "rigorously proven security guarantees" for incredibly fast and tightly optimized code.

Secure Page Table Monitor (SPTM): Architectural Prevention of Kernel Exploits

The Secure Page Table Monitor (SPTM) replaced the earlier Page Protection Layer (PPL), which, despite its intent, suffered from being a complex TCB where an attacker with a kernel read/write primitive could directly manipulate page tables and undermine code signing. The PPL's issues clustered around virtual address handling, incorrect pointer math, and loosely permitted invalid state transitions.

SPTM was designed as a "clean, least-privilege architecture" with day-zero engagement from offense and defense teams. It is logically and architecturally distinct from XNU, with code signing managed separately by TXM. Two key mechanisms underpin SPTM's security:

1. The Frame Table: This structure enforces valid state machine transitions as policy in data structures rather than distributed, error-prone code logic. This "inert data" approach allows policies to be validated centrally and systematically. The frame table's extensibility enables other powerful mitigations, such as XKR, which prevents private kernel memory from being mapped outside XNU and disallows multiple mappings of the same memory. XKR has proven effective against physical use-after-frees, copy-on-write bugs, and for tag confidentiality enforcement in MIE. The frame table policies also protect MIE tags from leaking.
2. Compiler and C Type System Integration: SPTM enlists the compiler to enforce centrally documented security invariants. Unsafe fields are "wrapped," and a central verification function performs all relevant security checks before returning the unwrapped type to the call site. Any attempt to directly access the wrapped type in code results in a compiler error, preventing an entire class of potential vulnerabilities at compile time.

Formal verification was also applied to aspects of SPTM's state machine management, particularly the definitions of valid frame type transitions. This has already uncovered "extremely subtle bugs" that would be very challenging for human auditors to find. Coupled with a development process requiring full root cause analysis for every bug, dedicated security reviews for every pull request, and continuous, rotating offensive engagement, SPTM architecturally prevents 95% of the PPL's original issues, with only a small set of "rare logic bugs" remaining. The success of SPTM, with no known in-the-wild exploits and only a single previously identified issue found during a six-month independent audit, demonstrates the power of rigorous security models and processes.

Memory Integrity Engine (MIE): Revolutionizing Memory Safety

MIE is Apple's ambitious project to make most memory safety bugs unexploitable and ensure that any remaining ones require completely custom, non-reusable exploitation strategies. The foundation of MIE is a precise memory corruption model, framed as an aggressor type with a bug attempting to corrupt a target type within a chosen distance delta. The attacker wins if they can place the aggressor within delta of the target. This model reveals two key defense levers: constraining the types and constraining delta.

MIE employs several mechanisms to achieve these goals:

• Type-Aware Sequestering: This constrains the types of objects that can be allocated together, making type confusion harder.
• Constraining Delta: MIE includes features to make it harder to predict object proximity in memory, even with control over allocation order. Allocation fronts ensure that new virtual memory assigned to the allocator becomes type-dependent.
• Enhanced MTE (Memory Tagging Extension): Apple assessed that the original ARM MTE specification allowed too much attacker flexibility, particularly with untagged memory. Their enhanced MTE adds "significant constraints" and separates all tags from each other. The kernel emulates the ARM checked pointer arithmetic ISA in software, ensuring that tagged memory can only affect other memory with the exact same tag. This, combined with canonical tagging, prevents first-order bugs in dynamic allocations from attacking kernel globals.
• Preventing Tag Deduction: A critical aspect is to prevent attackers from deducing correct tags. MIE ensures that memory sharing cannot reveal tags via the MTE ISA, and LDG and STG instructions will not work for this purpose. Reading/writing to shared memory bypasses tag checking to prevent tag leakage. Strong memory sharing protections are applied in the kernel and co-processors. Furthermore, Apple's silicon is carefully designed to perform speculative execution independent of tag values, a property validated in pre-silicon and on real hardware. This architecturally prevents timing side channels that have impacted other implementations, such as sticky tags and tick tag.
• Spectre v1 Mitigation: MIE includes a custom mitigation for Spectre v1, which could act as a data leaking side channel between EL0 and EL2. Similar to ideas from VUSC's TDI, this mitigation limits linear mappings and allocations to no more than 2 GB minus page size. This creates 4 GB gaps between different memory domains in the XNU address space, effectively making only "same-front speculation" possible and preventing speculation across domains.

Offensive Evaluation: A deeply comprehensive offensive evaluation effort was integrated from day zero. This included rebuilding six real-world exploit chains. For these chains, MIE made exploitation "not possible." Krstić highlighted that often, stopping just one step (e.g., step 3 of a 6-step LPE) was sufficient to invalidate the entire exploit strategy, as subsequent steps were completely custom and non-reusable. Even "stable, precise, pure logic bugs" requiring only a small memory corruption were deterministically broken by MIE. Offensive teams also researched novel techniques that could resist or survive MIE, such as crashing a target process, spraying aggressor objects, waiting for cleanup to create "imprints of holes," and then dropping an exploit payload to predictably fill those holes. This research led to immediate conclusions (e.g., CF objects not falling into the same bucket, Exxon Maloc not creating bump-order backing stores), giving Apple a multi-year head start in disabling such techniques before MIE shipped. The offensive team concluded that with MIE, viable memory corruption strategies are rare, generic techniques are almost impossible, many bug classes are unexploitable, and surviving bugs require "very fragile, completely custom corruptions every time."

Engineering Effort: Shipping MIE was a monumental engineering feat spanning five years and all of Apple. Kernel readiness work began in 2021 with software tools like KSAN and MTEAN. Userland readiness started in 2023 using Rosetta in ARM-to-ARM mode to address Objective C and language runtime issues. PGM (Probabilistic Guard Maloc), launched in 2021, was a four-year project to prepare system stability for MIE. At launch, iOS 26 ships with 150 processes and the kernel using MIE, with 70 in hard enforcement mode and the rest in telemetry-only mode to monitor stability and expand coverage over time.

A unique pre-ship task was finding all custom allocators on the system, as they could undermine MIE's security if not protected. Traditional methods like grep and even LLMs (85% accurate with too many false positives) proved inadequate. Apple developed a "very serious, precisely tuned classifier" using custom tokenization, vectorization, and principled component analysis (PCA), achieving 98.8% accuracy across the entire operating system to automatically identify these allocators.

Demo / Proof of Concept

▶ Watch: Practical challenges and complexity of the PPL (7:05)

This keynote did not feature a live demonstration or a traditional proof of concept. Instead, Ivan Krstić presented the results of extensive internal offensive evaluations and independent audits, providing compelling evidence of the effectiveness of the discussed security architectures and mitigations. The talk relied on architectural descriptions and quantitative outcomes from these rigorous testing processes to validate the claims made about Core Crypto, SPTM, and MIE.

Defensive Implications

▶ Watch: Introducing SPTM: a stronger, least privilege architecture (8:23)

The insights shared by Ivan Krstić offer critical implications for defenders striving to enhance the security posture of complex systems. The overarching message is a call to move beyond reactive patching to a proactive, scientifically grounded, and architecturally driven approach.

1. Embrace Formal Methods and Verification: For critical components like cryptographic libraries and kernel state machines, relying on intuition or traditional testing is insufficient. Defenders should invest in formal methods and computer-assisted proof tools (e.g., Saw, Cryptol, Isabel) to rigorously verify implementations against specifications, extending to highly optimized assembly code using custom tooling if necessary. This ensures correctness and the absence of subtle, hard-to-find bugs.
2. Integrate Offensive Research Early and Deeply: The "day zero engagement" model with offensive teams for SPTM and MIE is paramount. Defenders should establish processes where security researchers, particularly those with offensive expertise, are involved from the initial design phase through development and post-launch evaluation. This proactive integration helps identify architectural weaknesses, predict attack vectors, and validate mitigations before features ship, providing a significant "head start" against real-world threats.
3. Prioritize Architectural Security: Instead of incremental fixes, focus on fundamental architectural changes that prevent entire classes of vulnerabilities. The shift from PPL to SPTM, with its clean, least-privilege architecture and policy-driven frame table, serves as a prime example of how designing for security from the ground up can yield vastly superior outcomes, rendering 95% of prior issues architecturally impossible.
4. Leverage Compiler and Type Systems: Utilize compiler features and strong type systems to enforce security invariants at compile time. Wrapping unsafe fields and requiring central verification functions, as demonstrated with SPTM, can prevent common bug classes like incorrect pointer math and invalid state transitions from ever reaching runtime.
5. Develop Precise Threat Models: For complex areas like memory corruption, intuition is often incorrect. Defenders should invest in developing precise, quantifiable threat models (e.g., the aggressor/target/delta model for MIE) to guide the design of mitigations. This allows for a systematic approach to constraining attack surfaces, such as type-aware sequestering and allocation fronts.
6. Implement Comprehensive Memory Safety Mitigations: Beyond basic ASLR, adopt advanced memory tagging extensions (like Apple's enhanced MTE) and custom hardware/software mitigations for speculative execution vulnerabilities (e.g., Spectre v1). Ensure these mitigations separate memory domains, enforce tag integrity, and prevent tag deduction avenues.
7. Invest in Advanced Tooling for Code Discovery and Analysis: In large codebases, traditional methods fail. Develop or acquire sophisticated classifiers and analysis tools (e.g., the 98.8% accurate custom allocator classifier) to identify hidden attack surfaces or components that could undermine broader security features.
8. Balance Security with Stability and Performance: Recognize that deploying pervasive security features like MIE requires monumental engineering efforts to maintain system stability and performance. Utilize strategies like probabilistic guard allocators (PGM) and telemetry-only modes to gradually roll out and monitor new protections, ensuring a smooth transition for users.
9. Cultivate an Ethical Security Culture: Krstić's closing remarks underscore the moral dimension of security work. Defenders should ensure their work, and that of their colleagues, genuinely contributes to making the world a better place, protecting users and civil society, rather than enabling harm.

By adopting these principles, defenders can move towards building systems with "rigorously proven security guarantees" that are resilient against sophisticated, real-world threats, transforming security from a reactive struggle into a proactive, scientific endeavor.

Key Takeaways

• Security is Evolving Scientifically: Modern security is maturing by integrating scientific rigor—defining models and verifying correctness—with robust engineering, leading to unprecedented progress at the leading edge.
• Offensive Research is a Core Defensive Tool: Deep, day-zero integration of offensive research into the defense engineering loop is crucial for identifying architectural weaknesses, proactively countering attack techniques, and validating the effectiveness of mitigations.
• Formal Methods and Advanced Tooling are Catalysts: Tools like Saw, Cryptol, Isabel, and custom assembly verifiers, alongside sophisticated classifiers for code analysis, are powerful enablers for achieving high assurance and addressing complex security challenges.
• Architectural Shifts Prevent Entire Bug Classes: Designing clean, least-privilege architectures like SPTM, driven by policy in data structures and compiler-enforced invariants, can architecturally prevent a vast majority of vulnerabilities that plagued prior systems.
• Comprehensive Memory Safety is Achievable: Through precise memory corruption models, type-aware sequestering, enhanced MTE, and custom Spectre mitigations, it's possible to make most memory safety bugs unexploitable and surviving ones non-reusable.
• Incentivizing Research is Key: Significantly increased bounty rewards (up to $2 million for zero-click, $5 million theoretical maximum) and innovative verification methods like "target flags" are essential to encourage top-tier security research on increasingly hardened platforms.
• Ethical Responsibility is Paramount: Security professionals have a moral obligation to ensure their work benefits humanity, demanding that offensive capabilities are used to protect people, not to put them in harm's way.

About the Speaker(s)

Ivan Krstić is the Head of Security Engineering and Architecture (SEAR) at Apple. With nearly 30 years of experience in computer security, Krstić brings a deep historical perspective to the field, having learned to write his first toy exploit against a Solaris 7 machine almost 25 years ago. His role at Apple places him at the forefront of designing and implementing advanced security protections across the company's vast product ecosystem, from hardware to software. Krstić is a prominent voice advocating for a more scientific and ethically conscious approach to security, emphasizing the integration of offensive research into defensive strategies and the societal implications of security work.