Events & Conferences
Formal verification makes RSA faster — and faster to deploy
Most secure transactions online are protected by public-key encryption schemes like RSA, whose security depends on the difficulty of factoring large numbers. Public-key encryption improves security because it enables the encrypted exchange of private keys. But because it depends on operations like modular exponentiation of large integers, it introduces significant computational overhead.
Researchers and engineers have introduced all kinds of optimizations to make public-key encryption more efficient, but the resulting complexity makes it difficult to verify that the encryption algorithms are behaving properly. And a bug in an encryption algorithm can be disastrous.
This post explains how Amazon’s Automated Reasoning group improved the throughput of RSA signatures on Amazon’s Graviton2 chip by 33% to 94%, depending on the key size, while also proving the functional correctness of our optimizations using formal verification.
Graviton2 is a server-class CPU developed by Amazon Annapurna Labs, based on Arm Neoverse N1 cores. To improve the throughput of RSA signatures on Graviton2, we combined various techniques for fast modular arithmetic with assembly-level optimizations specific to Graviton2. To show that the optimized code is functionally correct, we formally verified it using the HOL Light interactive theorem prover, which was developed by a member of our team (John Harrison).
Our code is written in a constant-time style (for example, no secret-dependent branches or memory access patterns) to avoid side-channel attacks, which can learn secret information from operational statistics like function execution time. The optimized functions and their proofs are included in Amazon Web Services’ s2n-bignum library of formally verified big-number operations. The functions are also adopted by AWS-LC, the cryptographic library maintained by AWS, and by its bindings Amazon Corretto Crypto Provider (ACCP) and AWS Libcrypto for Rust (AWS-LC-RS).
| Key size (bits) | Baseline throughput (ops/sec) | Improved throughput (ops/sec) | Speedup (%) |
| 2048 | 299 | 541 | 81.00% |
| 3072 | 95 | 127 | 33.50% |
| 4096 | 42 | 81 | 94.20% |
Improvements in the throughput times of RSA signatures in AWS-LC on Graviton2.
Step 1. Making RSA fast on Graviton2
Optimizing the execution of RSA algorithms on Graviton2 requires the careful placement and use of multiplication instructions. On 64-bit Arm CPUs, the multiplication of two 64-bit numbers, with a product of up to 128 bits (conventionally designated 64×64→128), are accomplished by two instructions: MUL, producing the lower 64 bits, and UMULH, producing the upper 64 bits. On Graviton2, MUL has a latency of four cycles and stalls the multiplier pipeline for two cycles after issue, while UMULH has a latency of five cycles and stalls the multiplier pipeline for three cycles after issue. Since Neoverse N1 has a single multiplier pipeline but three addition pipelines, multiplication throughput is around one-tenth the throughput of 64-bit addition.
To improve throughput, we (1) applied a different multiplication algorithm, trading multiplication for addition instructions, and (2) used single-instruction/multiple-data (SIMD) instructions to offload a portion of multiplication work to the vector units of the CPU.
Algorithmic optimization
For fast and secure modular arithmetic, Montgomery modular multiplication is a widely used technique. Montgomery multiplication represents numbers in a special form called Montgomery form, and when a sequence of modular operations needs to be executed — as is the case with the RSA algorithm — keeping intermediary products in Montgomery form makes computation more efficient.
We implement Montgomery multiplication as the combination of big-integer multiplication and a separate Montgomery reduction, which is one of its two standard implementations.
On Graviton2, the benefit of this approach is that we can use the well-known Karatsuba algorithm to trade costly multiplications for addition operations. The Karatsuba algorithm decomposes a multiplication into three smaller multiplications, together with some register shifts. It can be performed recursively, and for large numbers, it’s more efficient than the standard multiplication algorithm.
We used Karatsuba’s algorithm for power-of-two bit sizes, such as 2,048 bits and 4,096 bits. For other sizes (e.g., 3072 bits), we still use a quadratic multiplication. The Karatsuba multiplication can be further optimized when the two operands are equal, and we wrote functions specialized for squaring as well.
With these optimizations we achieved a 31–49% speedup in 2,048- and 4,096-bit RSA signatures compared with our original code.
Microarchitectural optimization
Many Arm CPUs implement the Neon single-instruction/multiple-data (SIMD) architecture extension. It adds a file of 128-bit registers, which are viewed as vectors of various sizes (8/16/32/64 bit), and SIMD instructions that can operate on some or all of those vectors in parallel. Furthermore, SIMD instructions use different pipelines than scalar instructions, so both types of instructions can be executed in parallel.
Vectorization strategy. Vectorization is a process that replaces sequential executions of the same operation with a single operation over multiple values; it usually increases efficiency. Using SIMD instructions, we vectorized scalar 64-bit multiplications.
For big-integer multiplication, vectorized 64-bit multiply-low code nicely overlapped with scalar 64-bit multiply-high instructions (UMULH). For squaring, vectorizing two 64×64→128-bit squaring operations worked well. For multiplications occurring in Montgomery reduction, vectorizing 64×64→128-bit multiplications and 64×64→64 multiply-lows worked. To choose which scalar multiplications to vectorize, we wrote a script that enumerated differently vectorized codes and timed their execution. For short code fragments, exhaustive enumeration was possible, but for larger code fragments, we had to rely on experience. The overall solution was chosen only after extensive experiments with other alternatives, such as those described by Seo et. al. at ICISC’14.
Although the scalar and SIMD units are able to operate in parallel, it is sometimes necessary to move inputs and intermediate results between integer and SIMD registers, and this brings significant complications. The FMOV instruction copies data from a 64-bit scalar register to a SIMD register, but it uses the same pipeline as the scalar multiplier, so its use would reduce scalar-multiplier throughput.
The alternative of loading into a vector register first and then using MOV to copy it to a scalar register has lower latency, but it occupies the SIMD pipeline and hence lowers the throughput of SIMD arithmetic operations. Somewhat counterintuitively, the best solution was to make two separate memory loads into the integer and SIMD registers, with care for their relative placement. We did still use MOV instructions to copy certain SIMD results into integer registers when the SIMD results were already placed at SIMD registers because it was faster than a round trip via store-load instructions.
Fast constant-time table lookup code. Another independent improvement was the reimplementation of a vectorized constant-time lookup table for a fast modular-exponentiation algorithm. Combining this with our earlier optimization further raises our speedup to 80–94% when compared to the throughput of 2,048-/4,096-bit RSA signatures from our initial code, as well as a 33% speedup for 3,072-bit signatures.
Instruction scheduling. Even though Graviton2 is an out-of-order CPU, carefully scheduling instructions is important for performance, due to the finite capacity of components like reorder buffers and issue queues. The implementations discussed here were obtained by manual instruction scheduling, which led to good results but was time consuming.
We also investigated automating the process using the SLOTHY superoptimizer, which is based on constraint solving and a (simplified) microarchitecture model. With additional tweaks to Montgomery reduction to precalculate some numbers used in Karatsuba, SLOTHY optimization enabled a 95–120% improvement on 2,048-/4,096-bit throughputs and 46% on 3,072-bit! However, this method is not yet incorporated into AWS-LC since verifying the automated scheduling proved to be challenging. Studying the potential for automatically proving correctness of scheduling optimizations is a work in progress.
Step 2. Formally verifying the code
To deploy the optimized code in production we need to ensure that it works correctly. Random testing is a cheap approach for quickly checking simple and known cases, but to deliver a higher level of assurance, we rely on formal verification. In this section we explain how we apply formal verification to prove functional correctness of cryptographic primitives.
Introduction to s2n-bignum
AWS’s s2n-bignum is both (1) a framework for formally verifying assembly code in x86-64 and Arm and (2) a collection of fast assembly functions for cryptography, verified using the framework itself.
Specification in s2n-bignum. Every assembly function in s2n-bignum — including the new assembly functions used in RSA — has a specification stating its functional correctness. A specification states that for any program state satisfying some precondition, the output state of the program must satisfy some postcondition. For example, bignum_mul_4_8(uint64_t *z, uint64_t *x, uint64_t *y) is intended to multiply two 256-bit (four-word) numbers producing a 512-bit (eight-word) result. Its (abbreviated) precondition over an input state s is
aligned_bytes_loaded s (word pc) bignum_mul_4_8_mc ∧ read PC s = word pc ∧ C_ARGUMENTS [z, x, y] s ∧ bignum_from_memory (x,4) s = a ∧ bignum_from_memory (y,4) s = b
This means that the machine code of bignum_mul_4_8 is loaded at the address currently contained in the program counter PC (aligned_bytes_loaded), symbolic values are assigned to the function arguments according to C’s application binary interface (C_ARGUMENTS …), and big integers logically represented by the symbols a and b are stored in the memory location pointed to by x and y for four words (bignum_from_memory …).
The (abbreviated) postcondition over an output state s is
bignum_from_memory (z,8) s = a * b
This means that the multiplied result a * b is stored in the eight-word buffer starting at location z.
One more component is a relation between the input and output states that must be satisfied:
(MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI; MAYCHANGE [memory :> bytes(z,8 * 8)]) (s_in,s_out)
This means that executing the code may change registers/flags permitted by the application binary interface (ABI) and the eight-word buffer starting at z, but all other state components must remain unchanged.
Verifying assembly using HOL Light. To prove that the implementation is correct with respect to the specification, we use the HOL Light interactive theorem prover. In contrast to “black-box” automated theorem provers, tools like HOL Light emphasize a balance between automating routine proof steps and allowing explicit, and programmable, user guidance. When a proof exists on paper or inside someone’s head, a proficient user can effectively rewrite the proof in an interactive theorem prover. S2n-bignum uses a combination of two strategies to verify a program:
Symbolic execution. Given a representation of the input program state using symbolic variables in place of specific values, symbolic execution infers a symbolic output state at the end of some code snippet, in effect doing a more rigorous and generalized form of program execution. While this still leaves the postcondition to be proved, it strips away artifacts of program execution and leaves a purely mathematical problem.
Intermediate annotations in the style of Floyd-Hoare logic. Each intermediate assertion serves as a postcondition for the preceding code and a precondition for the subsequent code. The assertion need contain only the details that are necessary to prove its corresponding postcondition. This abstraction helps make symbolic simulation more tractable, in terms of both automated-reasoning capacity and the ease with which humans can understand the result.
We assume that the Arm hardware behaves in conformance with the model of s2n-bignum, but the model was developed with care, and it was validated by extensively cross-checking its interpretations against hardware.
Future formal-verification improvements. The formal verification for s2n-bignum does not yet cover nonfunctional properties of the implementation, including whether it may leak information through side channels such as the running time of the code. Rather, we handle this through a disciplined general style of implementation: never using instructions having variable timing, such as division, and no conditional branching/memory access patterns that depend on secret data. Also, we sanity-check some of these properties using simple static checks, and we execute the code on inputs with widely differing bit densities to analyze the corresponding run times and investigate any unexpected correlations.
These disciplines and sanity checks are standard practice with us, and we apply them to all the new implementations described here. In ongoing work, we are exploring the possibility of formally verifying the absence of information leakage.
Have you ever worked is legacy code? Are you curious what it takes to modernize systems at a massive scale?
Pascal Hartig is joined on the latest Meta Tech Podcast by Elaine and Buping, two software engineers working on a bold project to rewrite the decades-old C code in one of Meta’s core messaging libraries in Rust. It’s an ambitious effort that will transform a central messaging library that is shared across Messenger, Facebook, Instagram, and Meta’s AR/VR platforms.
They discuss taking on a project of this scope – even without a background in Rust, how they’re approaching it, and what it means to optimize for ‘developer happiness.’
Download or listen to the episode below:
You can also find the episode wherever you get your podcasts, including:
The Meta Tech Podcast is a podcast, brought to you by Meta, where we highlight the work Meta’s engineers are doing at every level – from low-level frameworks to end-user features.
Send us feedback on Instagram, Threads, or X.
And if you’re interested in learning more about career opportunities at Meta visit the Meta Careers page.
Amazon Research Awards (ARA) provides unrestricted funds and AWS Promotional Credits to academic researchers investigating various research topics in multiple disciplines. This cycle, ARA received many excellent research proposals from across the world and today is publicly announcing 73 award recipients who represent 46 universities in 10 countries.
This announcement includes awards funded under five call for proposals during the fall 2024 cycle: AI for Information Security, Automated Reasoning, AWS AI, AWS Cryptography, and Sustainability. Proposals were reviewed for the quality of their scientific content and their potential to impact both the research community and society. Additionally, Amazon encourages the publication of research results, presentations of research at Amazon offices worldwide, and the release of related code under open-source licenses.
Recipients have access to more than 700 Amazon public datasets and can utilize AWS AI/ML services and tools through their AWS Promotional Credits. Recipients also are assigned an Amazon research contact who offers consultation and advice, along with opportunities to participate in Amazon events and training sessions.
“Automated Reasoning is an important area of research for Amazon, with potential applications across various features and applications to help improve security, reliability, and performance for our customers. Through the ARA program, we collaborate with leading academic researchers to explore challenges in this field,” said Robert Jones, senior principal scientist with the Cloud Automated Reasoning Group. “We were again impressed by the exceptional response to our Automated Reasoning call for proposals this year, receiving numerous high-quality submissions. Congratulations to the recipients! We’re excited to support their work and partner with them as they develop new science and technology in this important area.”
“At Amazon, we believe that solving the world’s toughest sustainability challenges benefits from both breakthrough scientific research and open and bold collaboration. Through programs like the Amazon Research Awards program, we aim to support academic research that could contribute to our understanding of these complex issues,” said Kommy Weldemariam, Director of Science and Innovation Sustainability. “The selected proposals represent innovative projects that we hope will help advance knowledge in this field, potentially benefiting customers, communities, and the environment.”
ARA funds proposals throughout the year in a variety of research areas. Applicants are encouraged to visit the ARA call for proposals page for more information or send an email to be notified of future open calls.
The tables below list, in alphabetical order by last name, fall 2024 cycle call-for-proposal recipients, sorted by research area.
AI for Information Security
| Recipient | University | Research title |
| Christopher Amato | Northeastern University | Multi-Agent Reinforcement Learning Cyber Defense for Securing Cloud Computing Platforms |
| Bernd Bischl | Ludwig Maximilian University of Munich | Improving Generative and Foundation Models Reliability via Uncertainty-awareness |
| Shiqing Ma | University Of Massachusetts Amherst | LLM and Domain Adaptation for Attack Detection |
| Alina Oprea | Northeastern University | Multi-Agent Reinforcement Learning Cyber Defense for Securing Cloud Computing Platforms |
| Roberto Perdisci | University of Georgia | ContextADBench: A Comprehensive Benchmark Suite for Contextual Anomaly Detection |
Automated Reasoning
| Recipient | University | Research title |
| Nada Amin | Harvard University | LLM-Augmented Semi-Automated Proofs for Interactive Verification |
| Suguman Bansal | Georgia Institute of Technology | Certified Inductive Generalization in Reinforcement Learning |
| Ioana Boureanu | University of Surrey | Phoebe+: An Automated-Reasoning Tool for Provable Privacy in Cryptographic Systems |
| Omar Haider Chowdhury | Stony Brook University | Restricter: An Automatic Tool for Authoring Amazon Cedar Access Control Policies with the Principle of Least Privilege |
| Stefan Ciobaca | Alexandru Ioan Cuza University | An Interactive Proof Mode for Dafny |
| João Ferreira | INESC-ID | Polyglot Automated Program Repair for Infrastructure as Code |
| Sicun Gao | University Of California, San Diego | Monte Carlo Trees with Conflict Models for Proof Search |
| Mirco Giacobbe | University of Birmingham | Neural Software Verification |
| Tobias Grosser | University of Cambridge | Synthesis-based Symbolic BitVector Simplification for Lean |
| Ronghui Gu | Columbia University | Scaling Formal Verification of Security Properties for Unmodified System Software |
| Alexey Ignatiev | Monash University | Huub: Next-Gen Lazy Clause Generation |
| Kenneth McMillan | University of Texas At Austin | Synthesis of Auxiliary Variables and Invariants for Distributed Protocol Verification |
| Alexandra Mendes | University of Porto | Overcoming Barriers to the Adoption of Verification-Aware Languages |
| Jason Nieh | Columbia University | Scaling Formal Verification of Security Properties for Unmodified System Software |
| Rohan Padhye | Carnegie Mellon University | Automated Synthesis and Evaluation of Property-Based Tests |
| Nadia Polikarpova | University Of California, San Diego | Discovering and Proving Critical System Properties with LLMs |
| Fortunat Rajaona | University of Surrey | Phoebe+: An Automated-Reasoning Tool for Provable Privacy in Cryptographic Systems |
| Subhajit Roy | Indian Institute of Technology Kanpur | Theorem Proving Modulo LLM |
| Gagandeep Singh | University of Illinois At Urbana–Champaign | Trustworthy LLM Systems using Formal Contracts |
| Scott Stoller | Stony Brook University | Restricter: An Automatic Tool for Authoring Amazon Cedar Access Control Policies with the Principle of Least Privilege |
| Peter Stuckey | Monash University | Huub: Next-Gen Lazy Clause Generation |
| Yulei Sui | University of New South Wales | Path-Sensitive Typestate Analysis through Sparse Abstract Execution |
| Nikos Vasilakis | Brown University | Semantics-Driven Static Analysis for the Unix/Linux Shell |
| Ping Wang | Stevens Institute of Technology | Leveraging Large Language Models for Reasoning Augmented Searching on Domain-specific NoSQL Database |
| John Wawrzynek | University of California, Berkeley | GPU-Accelerated High-Throughput SAT Sampling |
AWS AI
| Recipient | University | Research title |
| Panagiotis Adamopoulos | Emory University | Generative AI solutions for The Spillover Effect of Fraudulent Reviews on Product Recommendations |
| Vikram Adve | University of Illinois at Urbana–Champaign | Fellini: Differentiable ML Compiler for Full-Graph Optimization for LLM Models |
| Frances Arnold | California Institute of Technology | Closed-loop Generative Machine Learning for De Novo Enzyme Discovery and Optimization |
| Yonatan Bisk | Carnegie Mellon University | Useful, Safe, and Robust Multiturn Interactions with LLMs |
| Shiyu Chang | University of California, Santa Barbara | Cut the Crap: Advancing the Efficient Communication of Multi-Agent Systems via Spatial-Temporal Topology Design and KV Cache Sharing |
| Yuxin Chen | University of Pennsylvania | Provable Acceleration of Diffusion Models for Modern Generative AI |
| Tianlong Chen | University of North Carolina at Chapel Hill | Cut the Crap: Advancing the Efficient Communication of Multi-Agent Systems via Spatial-Temporal Topology Design and KV Cache Sharing |
| Mingyu Ding | University of North Carolina at Chapel Hill | Aligning Long Videos and Language as Long-Horizon World Models |
| Nikhil Garg | Cornell University | Market Design for Responsible Multi-agent LLMs |
| Jessica Hullman | Northwestern University | Human-Aligned Uncertainty Quantification in High Dimensions |
| Christopher Jermaine | Rice University | Fast, Trusted AI Using the EINSUMMABLE Compiler |
| Yunzhu Li | Columbia University | Physics-Informed Foundation Models Through Embodied Interactions |
| Pattie Maes | Massachusetts Institute of Technology | Understanding How LLM Agents Deviate from Human Choices |
| Sasa Misailovic | University of Illinois at Urbana–Champaign | Fellini: Differentiable ML Compiler for Full-Graph Optimization for LLM Models |
| Kristina Monakhova | Cornell University | Trustworthy extreme imaging for science using interpretable uncertainty quantification |
| Todd Mowry | Carnegie Mellon University | Efficient LLM Serving on Trainium via Kernel Generation |
| Min-hwan Oh | Seoul National University | Mutually Beneficial Interplay Between Selection Fairness and Context Diversity in Contextual Bandits |
| Patrick Rebeschini | University of Oxford | Optimal Regularization for LLM Alignment |
| Jose Renau | University of California, Santa Cruz | Verification Constrained Hardware Optimization using Intelligent Design Agentic Programming |
| Vilma Todri | Emory University | Generative AI solutions for The Spillover Effect of Fraudulent Reviews on Product Recommendations |
| Aravindan Vijayaraghavan | Northwestern University | Human-Aligned Uncertainty Quantification in High Dimensions |
| Wei Yang | University of Texas at Dallas | Optimizing RISC-V Compilers with RISC-LLM and Syntax Parsing |
| Huaxiu Yao | University of North Carolina at Chapel Hill | Aligning Long Videos and Language as Long-Horizon World Models |
| Amy Zhang | University of Washington | Tools for Governing AI Agent Autonomy |
| Ruqi Zhang | Purdue University | Efficient Test-time Alignment for Large Language Models and Large Multimodal Models |
| Zheng Zhang | Rutgers University-New Brunswick | AlphaQC: An AI-powered Quantum Circuit Optimizer and Denoiser |
AWS Cryptography
| Recipient | University | Research title |
| Alexandra Boldyreva | Georgia Institute of Technology | Quantifying Information Leakage in Searchable Encryption Protocols |
| Maria Eichlseder | Graz University of Technology, Austria | SALAD – Systematic Analysis of Lightweight Ascon-based Designs |
| Venkatesan Guruswami | University of California, Berkeley | Obfuscation, Proof Systems, and Secure Computation: A Research Program on Cryptography at the Simons Institute for the Theory of Computing |
| Joseph Jaeger | Georgia Institute of Technology | Analyzing Chat Encryption for Group Messaging |
| Aayush Jain | Carnegie Mellon | Large Scale Multiparty Silent Preprocessing for MPC from LPN |
| Huijia Lin | University of Washington | Large Scale Multiparty Silent Preprocessing for MPC from LPN |
| Hamed Nemati | KTH Royal Institute of Technology | Trustworthy Automatic Verification of Side-Channel Countermeasures for Binary Cryptographic Programs using the HoIBA libary |
| Karl Palmskog | KTH Royal Institute of Technology | Trustworthy Automatic Verification of Side-Channel Countermeasures for Binary Cryptographic Programs using the HoIBA libary |
| Chris Peikert | University of Michigan, Ann Arbor | Practical Third-Generation FHE and Bootstrapping |
| Dimitrios Skarlatos | Carnegie Mellon University | Scale-Out FHE LLMs on GPUs |
| Vinod Vaikuntanathan | Massachusetts Institute of Technology | Can Quantum Computers (Really) Factor? |
| Daniel Wichs | Northeastern University | Obfuscation, Proof Systems, and Secure Computation: A Research Program on Cryptography at the Simons Institute for the Theory of Computing |
| David Wu | University Of Texas At Austin | Fast Private Information Retrieval and More using Homomorphic Encryption |
Sustainability
| Recipient | University | Research title |
| Meeyoung Cha | Max Planck Institute | Forest-Blossom (Flossom): A New Framework for Sustaining Forest Biodiversity Through Outcome-Driven Remote Sensing Monitoring |
| Jingrui He | University of Illinois at Urbana–Champaign | Foundation Model Enabled Earth’s Ecosystem Monitoring |
| Pedro Lopes | University of Chicago | AI-powered Tools that Enable Engineers to Make & Re-make Sustainable Hardware |
| Cheng Yaw Low | Max Planck Institute | Forest-Blossom (Flossom): A New Framework for Sustaining Forest Biodiversity Through Outcome-Driven Remote Sensing Monitoring |
AI safety is a priority at Amazon. Our investment in safe, transparent, and responsible AI (RAI) includes collaboration with the global community and policymakers. We are members of and collaborate with organizations such as the Frontier Model Forum, the Partnership on AI, and other forums organized by government agencies such as the National Institute of Standards and Technology (NIST). Consistent with Amazon’s endorsement of the Korea Frontier AI Safety Commitments, we published our Frontier Model Safety Framework earlier this year.
During the development of the Nova Premier model, we conducted a comprehensive evaluation to assess its performance and safety. This included testing on both internal and public benchmarks and internal/automated and third-party red-teaming exercises. Once the final model was ready, we prioritized obtaining unbiased, third-party evaluations of the model’s robustness against RAI controls. In this post, we outline the key findings from these evaluations, demonstrating the strength of our testing approach and Amazon Premier’s standing as a safe model. Specifically, we cover our evaluations with two third-party evaluators: PRISM AI and ActiveFence.
Evaluation of Nova Premier against PRISM AI
PRISM Eval’s Behavior Elicitation Tool (BET) dynamically and systematically stress-tests AI models’ safety guardrails. The methodology focuses on measuring how many adversarial attempts (steps) it takes to get a model to generate harmful content across several key risk dimensions. The central metric is “steps to elicit” — the number of increasingly sophisticated prompting attempts required before a model generates an inappropriate response. A higher number of steps indicates stronger safety measures, as the model is more resistant to manipulation. The PRISM risk dimensions (inspired by the MLCommons AI Safety Benchmarks) include CBRNE weapons, violent crimes, non-violent crimes, defamation, and hate, amongst several others.
Using the BET Eval tool and its V1.0 metric, which is tailored toward non-reasoning models, we compared the recently released Nova models (Pro and Premier) to the latest models in the same class: Claude (3.5 v2 and 3.7 non-reasoning) and Llama4 Maverick, all available through Amazon Bedrock. PRISM BET conducts black-box evaluations (where model developers don’t have access to the test prompts) of models integrated with their API. The evaluation conducted with BET Eval MAX, PRISM’s most comprehensive/aggressive testing suite, revealed significant variations in safety against malicious instructions. Nova models demonstrated superior overall safety performance, with an average of 43 steps for Premier and 52 steps for Pro, compared to 37.7 for Claude 3.5 v2 and fewer than 12 steps for other models in the comparison set (namely, 9.9 for Claude3.7, 11.5 for Claude 3.7 thinking, and 6.5 for Maverick). This higher step count suggests that on average, Nova’s safety guardrails are more sophisticated and harder to circumvent through adversarial prompting. The figure below presents the number of steps per harm category evaluated through BET Eval MAX.
The PRISM evaluation provides valuable insights into the relative safety of different Amazon Bedrock models. Nova’s strong performance, particularly in hate speech and defamation resistance, represents meaningful progress in AI safety. However, the results also highlight the ongoing challenge of building truly robust safety measures into AI systems. As the field continues to evolve, frameworks like BET will play an increasingly important role in benchmarking and improving AI safety. As a part of this collaboration Nicolas Miailhe, CEO of PRISM Eval, said, “It’s incredibly rewarding for us to see Nova outperforming strong baselines using the BET Eval MAX; our aim is to build a long-term partnership toward safer-by-design models and to make BET available to various model providers.” Organizations deploying AI systems should carefully consider these safety metrics when selecting models for their applications.
Manual red teaming with ActiveFence
The AI safety & security company ActiveFence benchmarked Nova Premier on Bedrock on prompts distributed across Amazon’s eight core RAI categories. ActiveFence also evaluated Claude 3.7 (non-reasoning mode) and GPT 4.1 API on the same set. The flag rate on Nova Premier was lower than that on the other two models, indicating that Nova Premier is the safest of the three.
| Model | 3P Flag Rate [↓ is better] |
| Nova Premier | 12.0% |
| Sonnet 3.7 (non-reasoning) | 20.6% |
| GPT4.1 API | 22.4% |
“Our role is to think like an adversary but act in service of safety,” said Guy Paltieli from ActiveFence. “By conducting a blind stress test of Nova Premier under realistic threat scenarios, we helped evaluate its security posture in support of Amazon’s broader responsible-AI goals, ensuring the model could be deployed with greater confidence.”
These evaluations conducted with PRISM and ActiveFence give us confidence in the strength of our guardrails and our ability to protect our customers’ safety when they use our models. While these evaluations demonstrate strong safety performance, we recognize that AI safety is an ongoing challenge requiring continuous improvement. These assessments represent a point-in-time snapshot, and we remain committed to regular testing and enhancement of our safety measures. No AI system can guarantee perfect safety in all scenarios, which is why we maintain monitoring and response systems after deployment.
Acknowledgments: Vincent Ponzo, Elyssa Vincent
-
Funding & Business6 days agoKayak and Expedia race to build AI travel agents that turn social posts into itineraries
-
Jobs & Careers6 days ago
Mumbai-based Perplexity Alternative Has 60k+ Users Without Funding
-
Mergers & Acquisitions6 days ago
Donald Trump suggests US government review subsidies to Elon Musk’s companies
-
Funding & Business6 days ago
Rethinking Venture Capital’s Talent Pipeline
-
Jobs & Careers6 days ago
Why Agentic AI Isn’t Pure Hype (And What Skeptics Aren’t Seeing Yet)
-
Funding & Business4 days ago
Sakana AI’s TreeQuest: Deploy multi-model teams that outperform individual LLMs by 30%
-
Jobs & Careers6 days ago
Astrophel Aerospace Raises ₹6.84 Crore to Build Reusable Launch Vehicle
-
Funding & Business7 days agoFrom chatbots to collaborators: How AI agents are reshaping enterprise work
-
Funding & Business4 days ago
Dust hits $6M ARR helping enterprises build AI agents that actually do stuff instead of just talking
-
Jobs & Careers6 days ago
Telangana Launches TGDeX—India’s First State‑Led AI Public Infrastructure
