# Galois Tools ## Featured Tools
CAMET ->Practical and powerful analysis tools to support Model-based DevOps, Digital Engineering, ACVIP, and more./files/jyeBYGOePpM1gr9iv7uR/spaces/nFCMxZvaanOBni4BM3Kq
Cryptol ->Domain-specific language for specifying cryptographic algorithms/files/ilvwrD4tjB9tBYpvizHU/spaces/PO8NU83T8kSMeYSiIV9h
SAW ->Provides the ability to formally verify properties of code written in C, Java, Rust, and Cryptol./files/Krxz8OFPQiyns7MepqZi/spaces/UApIrUvk02G42EmQuRHP
Swanky ->open source suite of Rust libraries for secure computation/files/PDzIOIxyAZVhcneBLPgU/spaces/wq6yofNUjxjFY0jrgli7
C2Rust ->Translates most C modules into semantically equivalent Rust code./files/V6AJ7B3rJorn0UntTfyN/spaces/11xJ6TZLGSMeaKYNw788
[Explore all Galois Tools on Github](https://github.com/GaloisInc/) -> # CAMET Library ## Overview CAMET® (pronounced "camay") stands for Curated Access to Model-based Engineering Tools. The CAMET Library provides system engineers with practical and powerful analysis tools to support Model-based DevOps, Digital Engineering, and the Architecture Centric Virtual Integration Process (ACVIP), and other modern development methodologies.
### Challenge As modern cyber-physical systems grow in scope and complexity, embedded software is responsible for the vast majority of the system’s functionality. Typically, testing and analysis for system-level requirements for embedded systems is not done until later stages of development when the cost to fix problems is orders of magnitude higher than fixing them in the earlier phases. These system-level requirements involve critical trade-offs between size, weight, power budgets, bandwidth and CPU utilization, which have significant ramifications on timing, as well as safety and security. ### Solution Galois’s CAMET® Library of model-based engineering tools helps system engineers and architects improve system capabilities and reduce the risk of cost and schedule overruns. CAMET supports the delivery of highly reliable, highly functional, safe and secure cyber-physical systems. The CAMET® Library was created to analyze and detect flaws in complex systems early on, during the requirements and design phases. CAMET’s powerful tools were developed with the support of SBIR awards from multiple agencies. Phase III SBIR support from the Army has matured them for use on the Future Vertical Lift program, one of the Army’s top modernization priorities. For a list of Model-Based Engineering Tools available in the CAMET Library, [click here](/camet/overview/camet-tools). ## Key Features * Tools that support continuous integration and testing for model-based engineering and analysis * Subscribers have access to all CAMET Library tools, software, models, and other materials * Each subscription provides access for up to five users * Supports modeling standards such as AADL, SysML, and [FACE](/camet/overview/face-tm-technical-standard) * User guides, example models, and instructional videos help new users get up and running * The CAMET Library analysis tools operate as plugins to the Open Source AADL Tool Environment (OSATE) * Selected CAMET Library tools operate as standalones via a standard Java API for use in any Java-friendly environment ## Subscription Each subscription provides access to all CAMET Library tools, software, models, and other materials. Enterprise support agreements, as well as new tools or functionality improvements, can be contracted separately. To learn more and subscribe, [click here](/camet/overview/subscription). ## [**Log In**](https://camet.adventium.com/users/sign_in) **→** # Training Resources ## Videos #### Getting Started
Introduction to the Architecture Centric Virtual Integration Process -> https://youtu.be/HE-Z0cKn4a4
SysML to AADL Bridge Tool
Overview -> https://youtu.be/W4IAnOXbg1g
#### Demos
Trade Space Tools Demo ->https://youtu.be/JHhp_S6OtSA
Framework for Analysis of Schedulability, Timing and Resources (FASTAR) Demo -> https://youtu.be/EFznuY2gh5s
RTOS Configuration File Generation Demo ->https://youtu.be/d4LIO_JkFSE
Multiple Independent Levels of Security (MILS) Demo ->https://youtu.be/43y5gV7ZS3k
Continuous Virtual Integration Toolkit (CVIT) Demo -> https://youtu.be/PuPm0GWxVHo
Model-based Analysis Using Domain Expertise (MAUDE) Demo ->https://youtu.be/VmaDyPoZ_zc
Stakeholder Access to Embedded System Models (SAESM) -> https://youtu.be/ZYE-SFVx8-g
Systems Engineering Safety and Security Analysis Framework (SESSAF)

SESSAF Installation Video

->

https://www.youtube.com/watch?v=vuj7SX4yuAA
Model Creation -> https://www.youtube.com/watch?v=qr4pppEo2sc

Adding Flows to the Model

->

https://www.youtube.com/watch?v=QNWdb6n6x4I
Safety Analysis -> https://www.youtube.com/watch?v=V1fsUdWluCw
## Additional Resources * [Paper: Applying ACVIP for Verification by Analysis during Airworthiness Qualification](https://apps.dtic.mil/sti/trecms/pdf/AD1202694.pdf) * [Paper: Airworthiness Qualification of ACVIP Tools](https://cdn.prod.website-files.com/673b407e535dbf3b547179dd/67706c3efd9cbe4e40eb38d8_2021-09-09_ACVIP-Airworthiness_v3_DistroA.pdf) * [Register for the Software Engineering Institute (SEI) online course, Modeling System Architectures Using the Architecture Analysis and Design Language (AADL)](https://www.sei.cmu.edu/education-outreach/courses/course.cfm?courseCode=V40) * [Publication: ACVIP: A Key Component of the DoD Digital Engineering Strategy](https://insights.sei.cmu.edu/library/architecture-centric-virtual-integration-process-acvip-a-key-component-of-the-dod-digital-engineering-strategy/) * [ACVIP Modeling & Analysis Handbook](https://cdn.prod.website-files.com/673b407e535dbf3b547179dd/6786ed77930332b4ced3988c_ACVIP-Modeling-%26-Analysis-Handbook_Mar2021_DistA.pdf) * [Authoritative Source of Truth Study (ASoT Study)](https://cdn.prod.website-files.com/673b407e535dbf3b547179dd/67706d222e6e6b63fe5b73f6_2021-03_AuthoritativeSourceOfTruthStudy_DEWG.pdf) * [Tools, Training, and Reference Materials for the FACE™ Technical Standard](https://www.opengroup.org/face/docsandtools) * [2018 Article: System Architecture Virtual Integration Nets Significant Savings, Software Engineering Institute, Carnegie Mellon University](https://insights.sei.cmu.edu/sei_blog/2018/05/analysis-system-architecture-virtual-integration-nets-significant-savings.html) * [Use Case: Joint Common Architecture Demonstration](https://tools.galois.com/camet/overview/www.galois.com/publications/joint-common-architecture-demonstration-shadow-architecture-centric-virtual-integration-process-final-technical-report) # CAMET Tools The CAMET® Library supports a range of modeling methodologies and technical standards throughout a project life-cycle, from system requirements through system integration. ## Overview The tools listed below have been designed to meet the complex demands of a modern model-based digital engineering environment, namely: * Integration of multiple analyses into a shared workflow. * Continuous virtual integration with mixed developer models. * Automated model verification, report generation, and code generation. *** ## CAMET Base Pack The CAMET Base Pack bundles the most-used CAMET Library tools in one download to simplify initial installation and use. It includes example models and full tool documentation.
For an example view of CAMET tools deployed on OSATE (Open Source AADL Tool Environment), watch [Getting Started with AADL Analysis Tools ](https://www.youtube.com/watch?v=kgcWPHwn93Y)(YouTube). To see how the SysML to AADL Bridge Tool allows SysML modelers to generate AADL for analysis, integration, and verification tasks in OSATE, watch [How to Translate from SysML to AADL](https://www.youtube.com/watch?v=ZM5-5Nz1G1k) (YouTube). *** ## Safety and Security Analysis ### RMF: Risk Management Framework *(Model Format: AADL)* The RMF Analysis tool analyzes models to reduce the risk that systems will fail certification under DoDI 8510.01 Risk Management Framework for DoD Information Technology (IT). The analysis answers the following questions: 1. Does the architecture isolate information flows with different criticalities? 2. Does the architecture place security controls everywhere they are needed? 3. Are the controls enforced as intended (non-bypassable and tamper-resistant)? For demonstrations please see these videos: * [RMF Mixed Criticality Analysis](https://www.youtube.com/watch?v=KFc3sElJXOc) * [RMF Step 4 Analysis](https://youtu.be/NNX03mcPtLQ) *** ### MILS: Multiple Independent Levels of Security *(Model Format: AADL)* The MILS tool analyzes AADL models to reduce the risk that systems will fail certification under DoDI 8540.01 Cross Domain Policy. It verifies that connected components operate at the same security level and that different security levels are separated with a protective measure like an air gap or an approved cross domain solution. To learn more, explore the following videos: * [About MILS: Explainer Video](https://www.youtube.com/watch?v=9qxscYg5xWc) * [MILS Security Analysis Tool for AADL Demo Video](https://youtu.be/43y5gV7ZS3k) *** ### SESSAF: Systems Engineering Safety and Security Analysis Framework (Model Format: AADL) SESSAF incorporates a top down analysis methodology aimed at identifying complex, multi-factor safety and security hazard scenarios, particularly in software reliant systems. It guides safety experts through a structured conversation, helping them methodically apply their domain knowledge to a specific system design. Using a wizard interface, the experts answer questions about safety and security concerns specific to the system design. Using the expert’s responses, SESSAF updates the AADL based system model which is then used by system engineers to address the findings and to generate customized reports. For demonstrations, please see these videos: * [How to Conduct a Safety Analysis](https://youtu.be/V1fsUdWluCw) * [How to Install SESSAF](https://youtu.be/vuj7SX4yuAA) * [How to Create an AADL Model](https://youtu.be/qr4pppEo2sc) * [How to Add Flows to an AADL Model](https://youtu.be/QNWdb6n6x4I) *** ### MADS: Multiple Analysis for Domain Separation *(Model Format: AADL)* The MADS tool helps engineers detect faults by assessing domain isolation in AADL system architecture models. Analyzing multiple classes of domain isolation simultaneously, developers can identify defects arising in one class due to model changes associated with a different class. *** ## Schedule Analysis and Generation ### FASTAR™ Compositional Schedulability Analysis *(Model Format: AADL)* FASTAR applies timing and resource analysis tools that support multiple scheduling methods and different types of equipment in order to provide end-to-end, system-wide analysis results. Supports MAST for distributed priority-scheduled systems, and SPICA for ARINC 653 scheduled systems. For a demonstration, please see this video: * [Framework for Analysis of Schedulability, Timing and Resources](https://youtu.be/DmBdnk0H18k) *** ### FASTAR™ Scheduler *(Model Format: AADL)* FASTAR generates schedules from a model of real-time embedded software systems. Schedules address thread and connection timing, demand requirements, and constraints on specified end-to-end flow latencies. Generates ARINC 653 schedules. *** ### RTOS: Real-Time Operating System Configuration *(Model Format: AADL)* RTOS generates RTOS-specific schedule configuration from an architecture model of the software components to be integrated in the target execution environment. The configuration is generated from a model that has already undergone analysis and verification using other tools. Supports LynxOS-178 RTOS. For a demonstration, please see this video: * [AADL Tools for Software/System Integration: ARINC 653 Schedules and RTOS Configuration Files](https://youtu.be/d4LIO_JkFSE) *** ### SPICA: Separation Platform for Integrating Complex Avionics *(Model Format: AADL)* SPICA has two core capabilities: schedule simulation and schedule generation. Specifically, it provides tools to generate ARINC653 partition schedules, and to analyze the timing of ARINC653 standard schedules. SPICA can be invoked on AADL models using either FASTAR or the Continuous Virtual Integration Toolkit. *** ## Behavioral Modeling ### SLICED: State Linked Interface Compliance Engine for Data *(Model Formats: AADL, FACE, and SysML implemented in MagicDraw)* SLICED allows system engineers to conduct behavioral analysis of models to detect errors in messaging patterns/paradigms, sampling rates, and latency requirements in embedded systems software. It combines timing analysis and Future Airborne Capability Environment (FACE™) data models with descriptions of the state of a software Unit of Portability (UoP). For demonstrations, please see these videos: * [Example use of SLICED for Behavior Analysis](https://youtu.be/DrgKwOu3eKE) * [Installation of SLICED in OSATE](https://youtu.be/DF9rogOOTRE) *** ## Workflow Automation ### SysML to AADL Bridge Tool *(Model Format: SysML, Enterprise Architect, and MagicDraw/Cameo supported)* The System Modeling Language (SysML) was developed for Model-Based Systems Engineering (MBSE). It has a broad scope that encompasses a range of systems, from civil engineering projects to organization operations. The Architecture Analysis and Design Language (AADL) was developed for embedded computer systems architectures and associated equipment. AADL provides standard semantics within the embedded computing domain, while SysML does not. Using AADL standard semantics in models enables a variety of existing computer system architecture analysis, integration, and testing tools to be applied to models. The SysML-to-AADL translation tool allows them to be used together in a collaborative and synergistic way: The strengths of SysML for overall systems engineering can be combined with the strengths of AADL for specifying and analyzing embedded computer subsystems within an overall system. Overview Video: [Automating the translation of SysML into AADL for Analysis](https://www.youtube.com/watch?v=W4IAnOXbg1g) Demonstration Video (external link): [How to Translate from SysML to AADL](https://youtu.be/TdD9idrnqqY) *** ### DSI: Design Space Investigator *(Model Format: AADL)* DSI provides provides an infrastructure, automation tools, and visualization tools that allow trade space analysis to be performed continuously as models are updated. DSI combines systems architecture specification and analysis technologies to support least commitment design of complex systems such as aircraft and spacecraft. When applied to system design, a least commitment approach helps developers avoid making premature design decisions that must later be retracted, thereby reducing or eliminating re-work costs. DSI helps developers make design decisions when necessary by automatically and continuously evaluating design alternatives throughout the development process. *** ### CVIT: Continuous Virtual Integration Toolkit CVIT Applies the software engineering concepts of continuous integration and testing to model-based engineering and analysis. CVIT allows users to stand up a server at their facility that automatically executes scripts for integration, analysis, and report generation of system models. Most CAMET Library analysis tools support CVIT, and instructions are included for adapting other tools to use CVIT. For a demonstration, please see this video: \ [Continuous Virtual Integration Server](https://youtu.be/PuPm0GWxVHo) *** ### INDIGO: INsight to Diverse Information Using Graphs and Ontologies *(Model Format: Web Ontology Language (OWL))* INDIGO provides capabilities to access multiple models and domain ontologies and explore relationships within sets of models developed in different languages using different tools. An enhanced browser recognizes access protocols and data in RDF formats to create a library of sources. Users select sets of models, interactively build queries supported by automated reasoning, with results displayed by choices of viewers. *** ## System Architecture and Implementation ### ISOSCELES™: Intrinsically Secure, Open, and Safe Control of Essential LayErS ISOSCELES is a reference architecture and set of development tools that enables developers to create safe and secure products, including Industrial Internet of Things (IIoT) systems, medical devices, and other embedded systems connected to a network, e.g., the Internet. Developers are able to focus on the functionality of their product with ISOSCELES providing the surrounding safety and security. ISOSCELES is compliant with cyber security best practices, FDA approval guidelines and security requirements, and California's IoT law effective January 2020. The reference architecture and documentation is open source and the development tools are available to sponsors of Adventium's CAMET Library. Support is available separately to integrate ISOSCELES into the system development workflow of its users. \ Further information: * [DHS Award Announcement Press Release](https://www.dhs.gov/science-and-technology/news/2016/02/02/dhs-st-awards-22m-medical-device-cyber-security-research) * [Star Tribune Article on Cyber-Vulnerability of Medical Devices](https://www.startribune.com/medical-devices-a-target-for-cyber-attacks-but-how-serious-is-the-threat/390761941/) # Subscription ## Requesting Access to CAMET Please contact us at to become a subscriber to Galois's CAMET® Library. Upon receipt of a subscription request email, Galois will provide instructions for access to CAMET library. Each subscription provides access to all CAMET Library tools, software, models, and other materials for the term selected. Enterprise Support, as well as new tools or functionality improvements, can be contracted separately. See below for Enterprise Support plans. With the CAMET subscription, the User agrees in full to the terms and conditions of the CAMET Library Terms of Use, and the End User License Agreements of the individual CAMET Library Software Tools. [CAMET Library Terms of Use](https://cdn.prod.website-files.com/673b407e535dbf3b547179dd/69c44b562f5a99c58fe3da24_CAMET_ToU_25March2026.pdf) [CAMET Software Tools: End User Agreement](https://cdn.prod.website-files.com/673b407e535dbf3b547179dd/69c44b8e7fefb6f20f02946d_FASTAR_EULA_CAMET_withDisclaimer_Updated25March2026.pdf)
## Subscription Levels *As of 1/1/2026, Galois changed the CAMET Library subscription model to the following:*
CAMET Library COST * FREE up to 10 users, per organization SUPPORT * Access to the self-service portal, with the option to purchase additional training and services
CAMET Enterprise COST * $18,000/seat/year, up to 5 seats * $15,000/seat/year for groups of 6–10 * $12,000/seat/year for groups larger than 10, less than 20 SUPPORT * Support provided for [CAMET Base Pack](/camet/overview/camet-tools#camet-base-pack) ONLY * Initial response to inbound support requests within 24 hours; available weekdays EST * Supported Onboarding * Each license will receive one seat to a Virtual Instructor-led Training * Access to the self-service portal * Includes license to CAMET Library
# FACE™ Technical Standard ### Tools, Training, and Reference Materials for the FACE™ Technical Standard The Architecture and Analysis Design Language (AADL) is an SAE International aerospace standard (AS) system model specification language (AS5506C) that supports various types of performance and safety analysis. The Future Airborne Capability Environment (FACE) Technical Standard defines a Reference Architecture intended for the development of portable software components targeted for general purpose, safety, and/or security purposes. The AADL Annex for the FACE Technical Standard Edition 3.0 (AS5506/4) provides guidelines for the integrated use of AADL and FACE Technical Standard data specifications and components. {% embed url="" %} # Cryptol: The Language of Cryptography ## What is Cryptol? Cryptol is a mathematically-focused programming language for creating, analyzing, and verifying complex cryptographic algorithms. Intuitive, expressive, and precise, Cryptol and its associated software tools allow you to describe algorithms in the language of mathematics and prove key security and other properties. [**View on GitHub**](https://github.com/GaloisInc/cryptol) [**Download**](/cryptol/get-started/download)
## Core Features, Capabilities, and Applications * **Expressive Syntax:** Cryptol’s high-level abstraction and intuitive syntax make it exceptionally expressive and ideal for rapid prototyping, refining, and analyzing cryptographic algorithms. * **Executable Specifications:** With Cryptol, users can create specifications that aren’t just theoretical models, but can be run as executable code. * **Formal Verification:** Cryptol allows users to test and verify specifications, while [SAW](https://tools.galois.com/saw/) extends this capability to verify implementations written in C, Java, and Cryptol. * **Scalable Security:** Cryptol and SAW automate much of the most time-consuming parts of formal verification, enabling the process to scale to complex systems * **Open Source Library:** Access specs for traditional and post-quantum cryptographic algorithms in our [open source ](https://github.com/GaloisInc/cryptol-specs)repository of Cryptol specifications. ## How Does It Work? **Bridging the Gap:** Cryptographic algorithms are typically represented in two forms: a non-executable mathematical notation for theoretical understanding (the “specification"), and a “reference implementation” for practical use. However, this approach presents a significant challenge: there isn’t an easy way to check the implementation against the mathematical specification to verify the correlation between the two and ensure it is correct and secure. **A New Paradigm:** Cryptol revolutionizes this process in two key ways. First, it enables engineers to create specifications of cryptographic algorithms (e.g., to generate cryptographic keys, encryption/decryption algorithms, hashing functions, etc.) that are executable, testable, and verifiable. From those specifications, users can generate their own test vectors, prove theorems, and more. Second, using Galois’s Software Analysis Workbench (SAW), it’s possible to prove the equivalence of performant, manually-written implementations to specifications. [**READ OUR DOCUMENTATION** ](/cryptol/get-started/documentation) ## Impact Cryptol and SAW have been used in national security, fintech, and cloud computing applications to keep citizens, systems, and data safe; secure financial transactions; and protect the privacy of millions of people across the globe. The high assurance approach they represent forms the backbone—both technologically and philosophically—of Galois’s larger effort to create trustworthiness in the most critical systems on the planet, and to maximize impact through sharing these powerful tools with the open source community. ## Open Source The R\&D community, industry, and the public at large can benefit when tools like Cryptol are open sourced. In addition, open-source tools can themselves benefit from and be independently verified by a broad, diverse user community. With this in mind, the U.S. Government and Galois agreed to open source Cryptol for broad application and public benefit, releasing the first fully public version in 2014. Now, Cryptol is open for anyone to use and explore, as is our open-source cryptographic library that includes specs for both traditional and post-quantum cryptographic algorithms. [**View the Cryptol Specs Repository on Github**](https://github.com/GaloisInc/cryptol-specs) # Documentation ### Reference Materials
Browse the Cryptol Reference Manual -> https://galoisinc.github.io/cryptol/master/RefMan.html
Read our Programming Cryptol guide -> https://cdn.prod.website-files.com/673b407e535dbf3b547179dd/677c422f88a92701db5a834d_ProgrammingCryptol.pdf
Access the web-based Cryptol course -> https://weaversa.github.io/cryptol-course/
### Publications Some of the material below was created for an earlier version of Cryptol. While the core ideas still apply to the current version, there have been some syntactic changes to the language, so some of the examples need to be translated to the current version. #### Case Studies and White Papers * [Empowering the Experts: High-Assurance, High-Performance, High-Level Design with Cryptol](https://cdn.prod.website-files.com/673b407e535dbf3b547179dd/67783b41108a7f20652ac9db_empowering_the_experts.pdf) * [Domain Specific Languages: A path to high assurance solutions](https://cdn.prod.website-files.com/673b407e535dbf3b547179dd/677c3dcf5de429e588c17875_Cryptol%20Case%20Study.pdf) * [CRYPTOL: High Assurance, Retargetable Crypto Development and Validation](https://cdn.prod.website-files.com/673b407e535dbf3b547179dd/677c3e237a1d1c47e020150e_Cryptol-%20High%20Assurance%2C%20Retargetable%20Crypto%20Development%20and%20Validation.pdf) #### Research Publications * Browning, S. and Weaver, P. Designing Tunable, Verifiable Cryptographic Hardware Using Cryptol. In [Design and Verification of Microprocessor Systems for High-Assurance](http://www.springer.com/engineering/circuits+&+systems/book/978-1-4419-1538-2), David S. Hardin, Editor. Springer 2010. * Colby Hoffman, Jeff Lewis, Brad Martin, Sally Browning, A Complete Design Flow for MILS in a Single High Assurance FPGA, European Reconfigurable Radio Technologies Workshop, 2010. * Levent Erkök, Magnus Carlsson, and Adam Wick. Hardware/Software Co-verification of Cryptographic Algorithms using Cryptol. In Formal Methods in Computer Aided Design Conference, FMCAD’09, Austin, TX, November 2009, IEEE. * Levent Erkök, John Matthews. High assurance programming in Cryptol. In CSIIRW’09: Proceedings of the 5th Annual Workshop on Cyber Security and Information Intelligence Research, Oak Ridge, TN, April 2009, ACM. * Levent Erkök and John Matthews. Pragmatic Equivalence and Safety Checking in Cryptol. PLPV 2009: 73-81. * Lee Pike, Mark Shields, John Matthews: A verifying core for a cryptographic language compiler. ACL2 2006: 1-10. # Open Source Cryptol is an open source project, hosted on GitHub, licensed under the three-clause BSD license. We believe that anyone who uses Cryptol is making an important contribution toward making Cryptol better. There are many ways to get involved. ## Explore
Read the Cryptol BlogRead the latest articles about Cryptolhttps://www.galois.com/news-insights?name=Cryptol
Cryptographic SpecificationsAccess the Cryptographic Libraryhttps://github.com/GaloisInc/cryptol-specs/tree/423fd3f381b3337c9d9ac52760019bf03f4314ae
GithubExplore the Github repositoryhttps://github.com/GaloisInc/cryptol
## How to Contribute ### Users If you write Cryptol programs that you think would benefit the community, fork the GitHub repository, and add them to the examples/contrib directory and submit a pull request. We host a Cryptol mailing list, which you can [join here](https://groups.google.com/a/galois.com/forum/#!forum/cryptol-users) If you run into a bug in Cryptol, if something doesn’t make sense in the documentation, if you think something could be better, or if you just have a cool use of Cryptol that you’d like to share with us, use the issues page on [GitHub](https://github.com/GaloisInc/cryptol), or send email to . ### Developers If you plan to do development work on the Cryptol interpreter, please make a fork of the GitHub repository and send along pull requests. This makes it easier for us to track development and to incorporate your changes.
# Download ## Download a Binary * [Linux (Ubuntu 22.04)](https://github.com/GaloisInc/cryptol/releases/download/3.5.0/cryptol-3.5.0-ubuntu-22.04-X64.tar.gz) ([GPG Signature](https://github.com/GaloisInc/cryptol/releases/download/3.5.0/cryptol-3.5.0-ubuntu-22.04-X64.tar.gz.sig)) * [Linux (Ubuntu 24.04)](https://github.com/GaloisInc/cryptol/releases/download/3.5.0/cryptol-3.5.0-ubuntu-24.04-X64.tar.gz) ([GPG Signature](https://github.com/GaloisInc/cryptol/releases/download/3.5.0/cryptol-3.5.0-ubuntu-24.04-X64.tar.gz.sig)) * [macOS 15 (ARM64)](https://github.com/GaloisInc/cryptol/releases/download/3.5.0/cryptol-3.5.0-macos-15-ARM64.tar.gz) ([GPG Signature](https://github.com/GaloisInc/cryptol/releases/download/3.5.0/cryptol-3.5.0-macos-15-ARM64.tar.gz.sig)) * [macOS 15 (X64)](https://github.com/GaloisInc/cryptol/releases/download/3.5.0/cryptol-3.5.0-macos-15-intel-X64.tar.gz) ([GPG Signature](https://github.com/GaloisInc/cryptol/releases/download/3.5.0/cryptol-3.5.0-macos-15-intel-X64.tar.gz.sig)) * [Windows](https://github.com/GaloisInc/cryptol/releases/download/3.5.0/cryptol-3.5.0-windows-2022-X64.tar.gz) ([GPG Signature](https://github.com/GaloisInc/cryptol/releases/download/3.5.0/cryptol-3.5.0-windows-2022-X64.tar.gz.sig)) Cryptol binaries for Mac OS X, Linux, and Windows are available from the [GitHub releases page](https://github.com/GaloisInc/cryptol/releases). Binaries are distributed as tarballs which you can extract to a location of your choice. The 3.x releases also include [optional downloads](https://github.com/GaloisInc/cryptol/releases/tag/3.4.0) including supported versions of several solvers. GPG signatures are available for each release, and we encourage you to [check the signature](http://gnupg.org/gph/en/manual/x135.html) against our [public key](https://cryptol.net/files/Galois.asc) before installing to ensure the integrity of the release you downloaded. Cryptol is also packaged using Docker and can be fetched using one of the following commands (for the REPL and RPC server, respectively): ``` docker pull ghcr.io/galoisinc/cryptol:3.5.0 docker pull ghcr.io/galoisinc/cryptol-remote-api:3.5.0 ``` ## Getting Z3 [Download Z3](https://github.com/Z3Prover/z3/releases) Cryptol currently depends on the [Z3 SMT solver](https://github.com/Z3Prover/z3/) to solve constraints during typechecking, and as the default solver for the `:sat` and `:prove` commands. You can download Z3 binaries for a variety of platforms from their [releases page](https://github.com/Z3Prover/z3/releases). Cryptol generally requires the most recent version of Z3, but you can see the specific version tested in CI by looking [here](https://github.com/GaloisInc/what4-solvers/releases/tag/snapshot-20260119). ### Getting other SMT Solvers Cryptol also integrates with the Yices, Boolector, CVC4, CVC5, and other SMT solvers. If you download and install them, you can select which one Cryptol uses as follows: `:set prover=cvc4`, `:set prover=yices`, etc. For a list of currently-supported solvers, see [the solvers we use in CI](https://github.com/GaloisInc/what4-solvers/releases/tag/snapshot-20250227) and the [SBV versions page](https://github.com/LeventErkok/sbv/blob/master/SMTSolverVersions.md). ### Licensing Terms Cryptol is licensed under a standard [3-clause BSD license](https://github.com/GaloisInc/cryptol/blob/master/LICENSE). # SAW: The Software Analysis Workbench ## What is SAW? The Software Analysis Workbench (SAW) is a tool that provides the ability to formally verify properties of code written in C, Java, Rust, and [Cryptol](/cryptol). It leverages automated SAT and SMT solvers to make this process as automated as possible, and provides a scripting language, called SAWScript, to enable verification to scale up to more complex systems. We also provide a remote procedure call (RPC) API and offer a [Python library](https://pypi.org/project/saw-client/) that interfaces with the RPC API. [**View on GitHub**](https://github.com/GaloisInc/saw-script) [**Download**](/saw/download/get-saw)
## Core Features and Capabilities * **Comprehensive Assurance:** As a formal verification tool, SAW is capable of showing that your program works on all inputs, not just the ones it was tested on, and is capable of finding counterexamples when code doesn’t agree with its specification. * **Scalable Security:** [Cryptol](/cryptol) and SAW automate much of the most time-consuming parts of formal verification, enabling the process to scale to complex systems. * **Open Source Library:** You can access the code for SAW in our [open source ](https://github.com/GaloisInc/saw-script)repository. ## How Does it Work? Behind the scenes, SAW leverages symbolic execution to translate code into formal models. During this process it executes code on symbolic inputs, effectively unrolling loops, and translating the code into a circuit representation. Symbolic execution is well suited to verifying code with bounded loops such as cryptographic verification. SAW is closely connected with [Cryptol](/cryptol), a domain-specific language Galois created for the high-level specification of cryptographic algorithms. The most common use of SAW is to prove equivalence between a Cryptol specification of an algorithm and a production implementation written in a language such as C or Java. [**READ OUR DOCUMENTATION** ](/saw/documentation/saw-tutorials-and-manual) ## Impact At Galois, we have used SAW primarily to verify implementations of cryptographic algorithms such as the [AES block cipher](http://en.wikipedia.org/wiki/Advanced_Encryption_Standard), the [Secure Hash Algorithm (SHA)](http://en.wikipedia.org/wiki/Secure_Hash_Algorithm), and [Elliptic Curve Digital Signature Algorithm (ECDSA)](http://en.wikipedia.org/wiki/Elliptic_Curve_Digital_Signature_Algorithm). We have used this to verify existing widely used libraries such as [libgcrypt](http://www.gnu.org/software/libgcrypt/) and [Bouncy Castle](https://www.bouncycastle.org/). We also have used SAW in collaboration with Amazon to prove the correctness of the HMAC implementation in their [s2n](https://github.com/awslabs/s2n) implementation of the TLS protocol. You can read more about that work [here](https://www.galois.com/articles/verifying-s2n-hmac-with-saw). More broadly, Cryptol and SAW have been used in national security, fintech, and cloud computing applications to keep citizens, systems, and data safe; secure financial transactions; and protect the privacy of millions of people across the globe. The high assurance approach they represent forms the backbone—both technologically and philosophically—of Galois’s larger effort to create trustworthiness in the most critical systems on the planet, and to maximize impact through sharing these powerful tools with the open source community. ## Open Source The R\&D community, industry, and the public at large can benefit when tools like SAW are open sourced. In addition, open-source tools can themselves benefit from and be independently verified by a broad, diverse user community. With this in mind, Galois has developed SAW as an open source tool from the very beginning, and the tool is open for anyone to use and explore. [**SAW SCRIPT REPO**](https://github.com/GaloisInc/saw-script) # SAW Tutorials and Manual SAW's tutorials and user manual are built and deployed to GitHub Pages as part of `saw-script`'s continuous integration system. We deploy versions for the `master` branch and all release/version tags (such that you can easily reference the documentation for the version(s) of SAW that you use). {% hint style="warning" %} Version-specific Web documentation will be available for SAW versions ≥ 1.3. For older versions, please see [the releases](https://github.com/GaloisInc/saw-script/releases), which include PDF renderings of the tutorials and manual for those versions. {% endhint %} Visit to view all available Web versions of the documentation. # Publications * "[Constructing semantic models of programs with the software analysis workbench](https://cdn.prod.website-files.com/673b407e535dbf3b547179dd/677c5403f423e08e322e135b_Constructing%20Semantic%20Models%20of%20Programs%20with%20The%20Software%20Analysis%20Workbench.pdf)" by Robert Dockins, Adam Foltzer, Joe Hendrix, Brian Huffman, Dylan McNamee, and Aaron Tomb * “[Verified Cryptographic Code for Everybody](https://link.springer.com/chapter/10.1007/978-3-030-81685-8_31)” by Brett Boston, Samuel Breese, Joey Dodds, Mike Dodds, Brian Huffman, Adam Petcher, and Andrei Stefanescu * “[Continuous Formal Verification of Amazon s2n](https://link.springer.com/chapter/10.1007/978-3-319-96142-2_26)” by Andrey Chudnov, Nathan Collins, Byron Cook, Joey Dodds, Brian Huffman, Colm MacCárthaigh, Stephen Magill, Eric Mertens, Eric Mullen, Serdar Tasiran, Aaron Tomb, and Eddy Westbrook # What is Crux? Crux is a tool for improving the assurance of software using **symbolic testing**, currently supporting C/C++ and Rust. Crux can provide you with additional assurance that your code does what you want it to do, and provides higher coverage of possible inputs than techniques such as randomized fuzzing or unit testing. Specifically, Crux uses symbolic reasoning to check tests **exhaustively**, on all possible inputs, rather than on a smaller number of fixed or randomly-chosen values. In this way, Crux improves the coverage possible with [property-based testing](https://www.drmaciver.com/2016/03/the-easy-way-to-get-started-with-property-based-testing/), a popular approach supported by [libraries](https://github.com/silentbicycle/theft) [for](https://en.wikipedia.org/wiki/QuickCheck) [many](https://blog.logrocket.com/property-based-testing-in-rust-with-proptest/) [languages](https://jsverify.github.io/). Crux can: * Perform **symbolic** reasoning to evaluate tests **exhaustively** * Analyze **C/C++** and **Rust** code * Generate **counter-examples** when tests fail * Generate **executable** versions of counter-examples to load in a debugger * Generate **complete** models of programs to comprehensively rule out failure cases Crux is available open-source under the 3-Clause BSD License [on GitHub](https://github.com/GaloisInc/crucible). # When should I use Crux? Crux tends to work well with small, critical segments of code that primarily perform computation, rather than interacting with the outside world. For example, it is well-suited to code such as cryptographic algorithms, network packet serialization, signal processing, and similar domains. When using Crux to ensure the absence of specific bugs, the code being analyzed should operate only over fixed-size data structures, and include only loops that will terminate after a bounded number of iterations, regardless of the contents of input data. However, Crux can still be useful for finding bugs in programs that operate over unbounded data or use unbounded loops. For larger programs, or programs where certain portions of code are missing, the [Software Analysis Workbench (SAW)](https://saw.galois.com) allows additional user input to divide programs into components and reason about those components more efficiently by considering them independently. # Download Crux * [Crux-LLVM (Ubuntu 22.04 64-bit)](https://github.com/GaloisInc/crucible/releases/download/crux-v0.12/crux-llvm-0.12-ubuntu-22.04-X64.tar.gz) ([GPG Signature](https://github.com/GaloisInc/crucible/releases/download/crux-v0.12/crux-llvm-0.12-ubuntu-22.04-X64.tar.gz.sig)) * [Crux-LLVM (Ubuntu 24.04 64-bit)](https://github.com/GaloisInc/crucible/releases/download/crux-v0.12/crux-llvm-0.12-ubuntu-24.04-X64.tar.gz) ([GPG Signature](https://github.com/GaloisInc/crucible/releases/download/crux-v0.12/crux-llvm-0.12-ubuntu-24.04-X64.tar.gz.sig)) * [Crux-LLVM (OSX Arm)](https://github.com/GaloisInc/crucible/releases/download/crux-v0.12/crux-llvm-0.12-macos-15-ARM64.tar.gz) ([GPG Signature](https://github.com/GaloisInc/crucible/releases/download/crux-v0.12/crux-llvm-0.12-macos-15-ARM64.tar.gz.sig)) * [Crux-LLVM (Windows 64-bit)](https://github.com/GaloisInc/crucible/releases/download/crux-v0.12/crux-llvm-0.12-windows-2022-X64.tar.gz) ([GPG Signature](https://github.com/GaloisInc/crucible/releases/download/crux-v0.12/crux-llvm-0.12-windows-2022-X64.tar.gz.sig)) * [Crux-MIR (Ubuntu 22.04 64-bit)](https://github.com/GaloisInc/crucible/releases/download/crux-v0.12/crux-mir-0.12-ubuntu-22.04-X64.tar.gz) ([GPG Signature](https://github.com/GaloisInc/crucible/releases/download/crux-v0.12/crux-mir-0.12-ubuntu-22.04-X64.tar.gz.sig)) * [Crux-MIR (Ubuntu 24.04 64-bit)](https://github.com/GaloisInc/crucible/releases/download/crux-v0.12/crux-mir-0.12-ubuntu-24.04-X64.tar.gz) ([GPG Signature](https://github.com/GaloisInc/crucible/releases/download/crux-v0.12/crux-mir-0.12-ubuntu-24.04-X64.tar.gz.sig)) * [Crux-MIR (OSX Arm)](https://github.com/GaloisInc/crucible/releases/download/crux-v0.12/crux-mir-0.12-macos-15-ARM64.tar.gz) ([GPG Signature](https://github.com/GaloisInc/crucible/releases/download/crux-v0.12/crux-mir-0.12-macos-15-ARM64.tar.gz.sig)) Crux binaries for Linux, macOS, and Windows are available from the GitHub [releases page](https://github.com/GaloisInc/crucible/releases). Binaries are distributed as tarballs which you can extract to a location of your choice. Note that Crux-MIR binaries for Windows are not currently included, but we expect to include them in an upcoming release. GPG signatures are available for each release, and we encourage you to [check the signature](http://gnupg.org/gph/en/manual/x135.html) against our [public key](https://app.gitbook.com/o/OKpco5V1fngn2MK4lcSF/s/UApIrUvk02G42EmQuRHP/crux/pgp-public-key) before installing to ensure the integrity of the release you downloaded. Crux is also packaged using Docker, and can be fetched using one of the following commands: ``` docker pull ghcr.io/galoisinc/crux-llvm:0.12 docker pull ghcr.io/galoisinc/crux-mir:0.12 ``` Use the following command to run `crux-mir` through `cargo crux-test` from Docker on the Cargo project in the current directory: ``` docker run --rm -it --mount type=bind,source=$(pwd),target="/crux-mir/workspace" ghcr.io/galoisinc/crux-mir:0.12 ``` ### Dependencies Crux requires a companion tool, `mir-json`, which provides a Cargo plugin and `rustc` wrapper. We recommend installing `mir-json` directly with Cargo by following the instructions in the [`mir-json` README](https://github.com/GaloisInc/mir-json/blob/master/README.md). Crux can make use of a variety of external SMT solvers, including Boolector, CVC4, CVC5, Yices, and Z3. These solvers can be downloaded from their respective developers at the locations below. * [Boolector](http://fmv.jku.at/boolector/) from Johannes Kepler University Linz * [CVC4](https://cvc4.github.io/) from New York University * [CVC5](https://cvc5.github.io/) from Stanford University and the University of Iowa * [Yices](http://yices.csl.sri.com/) from SRI International * [Z3](https://github.com/Z3Prover/z3/releases) from Microsoft Research # PGP Public Key ``` -----BEGIN PGP PUBLIC KEY BLOCK----- mQINBGKCqukBEAC5L3c5MYpH3GL/DHI57mazcvh1INQUWlIn+yWdIitVDq/Epj6h eQYMh5kdoVzy8nZIYLCOLTjgP3MBaY+Y3UmpmMCdhMSKpPXx5RMKN0y9+N9Uh6RQ 2bu6VjYqnm4LnLRJ8bGw+Ve56ysQMhzYpLan3j2Vcne+X1qaDPVhZJGmAdQztCLo paGp75Rtq1sO0fxBZ7hnh2aTXSS4DE25AsVQjnpQXGS3l/pxK6dNQIY9uB153bCd Uxrkod0wLICObo1WZvSAc690jeBSvspLPxfgri8p7ZxwQ9Z/X4tDxchDUcAZIYR4 Iz0JsIi2OSBLZIYD9wrsw/GvSPXHPi7n4gJz5K5lR9mCzcSOdavI3Kiqt1JaLljy I+Q10AZPowyL2JymYRxa8R/ACV8pDCBhp64jBOyS7AtUXBbwoPQ72ppNUTP/OgSI JH+YanKnwA7mFyS7XUtyyfadJ+scer6Opg5ATcIoRJ5vWMi9gIe5waNfM3PJPSq1 me8cFHB3tiajSm1HqonMaZIbQdphiIVDCPlUXflmWdfjOctsUo4m8x9izRJqNk8M 0KPQGRQCA1+3l4XXTzFWAq09RgBH1aZcPA2Mp2k2oxfC7wjXXDyw+9MysrSGkfXX B+5a9KQlHoJYTJv7fWk271HlJdnkRTbHunfWDYpGHmi7WhNxijU4UeUTgQARAQAB tDlHYWxvaXMgQ3J5cHRvbCAoQ3J5cHRvbCBSU0EgU2lnbmluZykgPGNyeXB0b2xA Z2Fsb2lzLmNvbT6JAlgEEwEIAEIWIQQH/JDQyT9fO1Y1Th3L9LtBQ9tKOgUCYoKq 6QIbAwUJEswDAAULCQgHAgMiAgEGFQoJCAsCBBYCAwECHgcCF4AACgkQy/S7QUPb SjoyYRAAnxed7FwVF/8py1vHvWB/NwEdUw4KHhNTBC1JK2Q1bj1CkdMhTLqKqAFP Dak+BYhOFq4b5GxMfJWkW+p9dzsavDd1Cgb7JIllNE4WejNPEwgrIxwPMdZAmTGw WNyWk9fTlTBm6RqNUiSd++SprukfF+AIJ49iY65KUC4hL7rxx6JSUR/uu9J0HDPV YhhsvjwnR+fR0HSbU0Vs2hETwR9AGM24OGnEn0tQ4PW6TtHkbFngVh1bUB6eDMzi qyrOueLPpnXme7I3FJg0J8c6Te+tydEomJ6CmClQxzCeuGs0O526WLpkLazX3p0Z UZjjdhS+g6anBA3pTa9bXbCBQVxuQ8grGGLHkpELpPpc55cnCtVBxhP0KlwbniyE gQaKQtxoMZ/P3E6DOSLfoo8PFO6RonDlxke+ZI1VrHlztoXBDEoUSRJVg57lFvYn /HXl98BaXr5CI5ycAf68YrMZ68iZ2VXYrnO7yfphd1xE1aGQzoMyKUztLuwbH+q2 0PIQ9pzbmkVmCGFK1ExJu5RNRuWN7IkUMWNpyyFZSocZqaKGpbtsEvFM5Gaiw942 pn2D/e/GhcdqdjpitpiAtv8H4CpSzQO72xgEy/trH29AkrKtfOVdnLgpw/J9Knc/ c4iJXzWyylT87D9sQvLSNoez9VcN4sMg6xIwIO1wp72Fox9ab/q5Ag0EYoKq6QEQ ANhnpUZuy0ouXsQn8ppozMm3KJvOc4b9Lq2TREG0kXhJsidNiDz3PeASRAbPhjnv nRAAbLEC4ZhjE74ukLbB7xnWEqqovYAXMghbJz6+pkNDjduhxm1mwDpmZBd+xDsW ACred5NpkMdwKU8puQLDT/Y9j7tLlZ0x1RmK/cOIm1oG03QMqbYnkrkWQoVgz1sF bYzDTIB9bYvdrrB7AL8g81XZmCtzFv01YG7vIwkAgS9XDbnXD+zWWenNi38s8k5S +POiExOePL3+dORWKNmRiMoiFV7/rk56TbvRmGZAeo0zZ2Cv1ojpaDKTX4vk2QJ+ nbH+rmKHso2g7GiGf1tFytMQmfF6h+ztjCMiqgKGKpVECfvKB5IwyP+A2m/Z4NNJ DEPeT3XaXFiUaW3RC9e1dPGkZw+CY+GXlmtCMyTsWNbTNjt7snt4yF9Ukex1xt0W 91Gm7pcbLQeOn4bGOMbqaKtUAOUiZYjawaTrwXSLWHVQfabd7bwa/wg+Z4RZV/LU /jW3V6ZFaMDZUg3y0Gzh/K3ow+VdFgKAKXLDCtEJsdVBmCNhu61ZYaX/EXqhDoLi yffVFxvo+bl3qE1mNbOW838t3jk4LBMHHwT0ZJ9WfQRAFpAcpWm2smonaIFOBvNG epdFjywIR7i33h1wMODsAASpy8RNz/VS0TzdM03DFos1ABEBAAGJAjwEGAEIACYW IQQH/JDQyT9fO1Y1Th3L9LtBQ9tKOgUCYoKq6QIbDAUJEswDAAAKCRDL9LtBQ9tK OthkD/4wm0PCXAVZugwQdmMKkQYp1xcC99W6CzK0fDYYx7FkFO28EabnTMEB9aFT /aAqouwu6BpHjVrNv/82Jla3ZQPHoy0QMTQQEFmJs3Ii5VGYlHGw2fnn7171Vffj 3qqbaPNULV5x5lS/kmi9n8ctImfu/TdDIezv/2gRc2Gu4I5OcMlTRcPViPt9mQbl 6vjsS/2pCtuuB1SRN4+qJpqHCSWGyAJDY14uNhgfxqPwC5z5YZp7NYnD1ZfCE2Vq EQp4Kijf8L8oeGPpkYqjLFHJgJBGr4AGiKYzx8ETV9MIGCsDsAsAeQYn9EFYtuOf qqS0itP+MtwEqS74zQ+leDrP6nPSr8wLpYVUo/R8pTv/0Q8nvM/nDShDjv6Etmkp XOZZ7ZJOO57exT6W2fpZt12T3N19lblKRC0YuJpWaw8RhAvAcXx7BgcEPRb9JVWk 6XvyJ+Tl3pgL6RXUSTIglRci6QnVOh7gIGb9m9LGqadOlSjcUmpcPcyGq0jsm6oJ nHdsF+ebaqB+LqapEv+TmN9b4CXVP2DoMSYfD+FffESaM99IapjyrsrfIpN2Gz7M Mlt7hiEt0V5OX88e8yGVSEVShQrJf0IJmK8T7ZFr0TuvrvRt67mIxY55sgarwuAG fivwqr2HwvnbXI1+nlXWQhDWykKQIw4QWEO0PsOPfULLB+eEog== =dmYY -----END PGP PUBLIC KEY BLOCK----- ``` # Overview SAW is an open source project, hosted on GitHub, licensed under the 3-clause BSD license. We believe that anyone who uses SAW is making an important contribution toward making the tool better. There are many ways to get involved. ### [Explore the Github Repository](https://github.com/GaloisInc/saw-script) # How to Contribute SAW is in active development. At Galois, we are passionate about improving the security and safety of critical software, and we think that verification tools such as SAW have an important role in achieving that goal. We would love feedback on how to make SAW better. Please contact us at if you have any questions about SAW or high assurance development in general. If you encounter any issues using SAW, please file a [ticket on GitHub](https://github.com/galoisinc/saw-script/issues). # Get SAW ## Download a Binary * [Linux (Ubuntu 22.04)](https://github.com/GaloisInc/saw-script/releases/download/v1.5/saw-1.5-ubuntu-22.04-X64.tar.gz) ([GPG Signature](https://github.com/GaloisInc/saw-script/releases/download/v1.5/saw-1.5-ubuntu-22.04-X64.tar.gz.sig)) * [Linux (Ubuntu 24.04)](https://github.com/GaloisInc/saw-script/releases/download/v1.5/saw-1.5-ubuntu-24.04-X64.tar.gz) ([GPG Signature](https://github.com/GaloisInc/saw-script/releases/download/v1.5/saw-1.5-ubuntu-24.04-X64.tar.gz.sig)) * [macOS 15 (X64)](https://github.com/GaloisInc/saw-script/releases/download/v1.5/saw-1.5-macos-15-intel-X64.tar.gz) ([GPG Signature](https://github.com/GaloisInc/saw-script/releases/download/v1.5/saw-1.5-macos-15-intel-X64.tar.gz.sig)) * [macOS 15 (ARM64)](https://github.com/GaloisInc/saw-script/releases/download/v1.5/saw-1.5-macos-15-ARM64.tar.gz) ([GPG Signature](https://github.com/GaloisInc/saw-script/releases/download/v1.5/saw-1.5-macos-15-ARM64.tar.gz.sig)) * [Windows](https://github.com/GaloisInc/saw-script/releases/download/v1.5/saw-1.5-windows-2022-X64.tar.gz) ([GPG Signature](https://github.com/GaloisInc/saw-script/releases/download/v1.5/saw-1.5-windows-2022-X64.tar.gz.sig)) SAW binaries for Linux and macOS are available from the GitHub [releases page](https://github.com/GaloisInc/saw-script/releases). Binaries are distributed as .tar.gz or .zip files which you can extract to a location of your choice. Nightly builds are also available [here](https://github.com/GaloisInc/saw-script/actions?query=event%3Aschedule). GPG signatures are available for each release, and we encourage you to [check the signature](http://gnupg.org/gph/en/manual/x135.html) against our [public key](/saw/download/get-saw/public-key) before installing to ensure the integrity of the release you downloaded. SAW is also available for [Docker](https://github.com/orgs/galoisinc/packages/container/package/saw) and can be fetched using one of the following commands (for the REPL and RPC API, respectively): ```docker docker pull ghcr.io/galoisinc/saw:1.5 docker pull ghcr.io/galoisinc/saw-remote-api:1.5 ``` Nightly versions of the Docker images are also available: ```docker docker pull ghcr.io/galoisinc/saw:nightly docker pull ghcr.io/galoisinc/saw-remote-api:nightly ``` ## Dependencies SAW can make use of a variety of external tools, particularly SMT solvers. Due to SAW’s use of [Cryptol](/cryptol), the Z3 solver is a strict dependency for Cryptol type checking. The full set of SMT solvers we currently support for other verification tasks is determined by Levent Erkök’s [SBV](http://hackage.haskell.org/package/sbv) package and Galois’ [What4](https://github.com/galoisinc/what4) package. This set currently includes ABC, Boolector, CVC4, CVC5, MathSAT, Yices, and Z3. These solvers can be downloaded from their respective developers at the locations below. * [ABC](https://github.com/berkeley-abc/abc) from UC Berkeley * [Boolector](http://fmv.jku.at/boolector/) from Johannes Kepler University Linz * [CVC4](http://cvc4.cs.nyu.edu/downloads/) from New York University * [CVC5](https://cvc5.github.io/) from Stanford University and the University of Iowa * [MathSAT](http://mathsat.fbk.eu/download.html) from Fondazione Bruno Kessler * [Yices](http://yices.csl.sri.com/) from SRI International * [Z3](https://github.com/Z3Prover/z3/releases) from Microsoft Research As of release v1.1, we also provide binary packages for SAW that include compatible versions of a variety of solvers. Look for archive files that have with-solvers in the filename on the [v1.5 release page](https://github.com/GaloisInc/saw-script/releases/tag/v1.4).
# Public Key ``` -----BEGIN PGP PUBLIC KEY BLOCK----- mQINBGKCqukBEAC5L3c5MYpH3GL/DHI57mazcvh1INQUWlIn+yWdIitVDq/Epj6h eQYMh5kdoVzy8nZIYLCOLTjgP3MBaY+Y3UmpmMCdhMSKpPXx5RMKN0y9+N9Uh6RQ 2bu6VjYqnm4LnLRJ8bGw+Ve56ysQMhzYpLan3j2Vcne+X1qaDPVhZJGmAdQztCLo paGp75Rtq1sO0fxBZ7hnh2aTXSS4DE25AsVQjnpQXGS3l/pxK6dNQIY9uB153bCd Uxrkod0wLICObo1WZvSAc690jeBSvspLPxfgri8p7ZxwQ9Z/X4tDxchDUcAZIYR4 Iz0JsIi2OSBLZIYD9wrsw/GvSPXHPi7n4gJz5K5lR9mCzcSOdavI3Kiqt1JaLljy I+Q10AZPowyL2JymYRxa8R/ACV8pDCBhp64jBOyS7AtUXBbwoPQ72ppNUTP/OgSI JH+YanKnwA7mFyS7XUtyyfadJ+scer6Opg5ATcIoRJ5vWMi9gIe5waNfM3PJPSq1 me8cFHB3tiajSm1HqonMaZIbQdphiIVDCPlUXflmWdfjOctsUo4m8x9izRJqNk8M 0KPQGRQCA1+3l4XXTzFWAq09RgBH1aZcPA2Mp2k2oxfC7wjXXDyw+9MysrSGkfXX B+5a9KQlHoJYTJv7fWk271HlJdnkRTbHunfWDYpGHmi7WhNxijU4UeUTgQARAQAB tDlHYWxvaXMgQ3J5cHRvbCAoQ3J5cHRvbCBSU0EgU2lnbmluZykgPGNyeXB0b2xA Z2Fsb2lzLmNvbT6JAlgEEwEIAEIWIQQH/JDQyT9fO1Y1Th3L9LtBQ9tKOgUCYoKq 6QIbAwUJEswDAAULCQgHAgMiAgEGFQoJCAsCBBYCAwECHgcCF4AACgkQy/S7QUPb SjoyYRAAnxed7FwVF/8py1vHvWB/NwEdUw4KHhNTBC1JK2Q1bj1CkdMhTLqKqAFP Dak+BYhOFq4b5GxMfJWkW+p9dzsavDd1Cgb7JIllNE4WejNPEwgrIxwPMdZAmTGw WNyWk9fTlTBm6RqNUiSd++SprukfF+AIJ49iY65KUC4hL7rxx6JSUR/uu9J0HDPV YhhsvjwnR+fR0HSbU0Vs2hETwR9AGM24OGnEn0tQ4PW6TtHkbFngVh1bUB6eDMzi qyrOueLPpnXme7I3FJg0J8c6Te+tydEomJ6CmClQxzCeuGs0O526WLpkLazX3p0Z UZjjdhS+g6anBA3pTa9bXbCBQVxuQ8grGGLHkpELpPpc55cnCtVBxhP0KlwbniyE gQaKQtxoMZ/P3E6DOSLfoo8PFO6RonDlxke+ZI1VrHlztoXBDEoUSRJVg57lFvYn /HXl98BaXr5CI5ycAf68YrMZ68iZ2VXYrnO7yfphd1xE1aGQzoMyKUztLuwbH+q2 0PIQ9pzbmkVmCGFK1ExJu5RNRuWN7IkUMWNpyyFZSocZqaKGpbtsEvFM5Gaiw942 pn2D/e/GhcdqdjpitpiAtv8H4CpSzQO72xgEy/trH29AkrKtfOVdnLgpw/J9Knc/ c4iJXzWyylT87D9sQvLSNoez9VcN4sMg6xIwIO1wp72Fox9ab/q5Ag0EYoKq6QEQ ANhnpUZuy0ouXsQn8ppozMm3KJvOc4b9Lq2TREG0kXhJsidNiDz3PeASRAbPhjnv nRAAbLEC4ZhjE74ukLbB7xnWEqqovYAXMghbJz6+pkNDjduhxm1mwDpmZBd+xDsW ACred5NpkMdwKU8puQLDT/Y9j7tLlZ0x1RmK/cOIm1oG03QMqbYnkrkWQoVgz1sF bYzDTIB9bYvdrrB7AL8g81XZmCtzFv01YG7vIwkAgS9XDbnXD+zWWenNi38s8k5S +POiExOePL3+dORWKNmRiMoiFV7/rk56TbvRmGZAeo0zZ2Cv1ojpaDKTX4vk2QJ+ nbH+rmKHso2g7GiGf1tFytMQmfF6h+ztjCMiqgKGKpVECfvKB5IwyP+A2m/Z4NNJ DEPeT3XaXFiUaW3RC9e1dPGkZw+CY+GXlmtCMyTsWNbTNjt7snt4yF9Ukex1xt0W 91Gm7pcbLQeOn4bGOMbqaKtUAOUiZYjawaTrwXSLWHVQfabd7bwa/wg+Z4RZV/LU /jW3V6ZFaMDZUg3y0Gzh/K3ow+VdFgKAKXLDCtEJsdVBmCNhu61ZYaX/EXqhDoLi yffVFxvo+bl3qE1mNbOW838t3jk4LBMHHwT0ZJ9WfQRAFpAcpWm2smonaIFOBvNG epdFjywIR7i33h1wMODsAASpy8RNz/VS0TzdM03DFos1ABEBAAGJAjwEGAEIACYW IQQH/JDQyT9fO1Y1Th3L9LtBQ9tKOgUCYoKq6QIbDAUJEswDAAAKCRDL9LtBQ9tK OthkD/4wm0PCXAVZugwQdmMKkQYp1xcC99W6CzK0fDYYx7FkFO28EabnTMEB9aFT /aAqouwu6BpHjVrNv/82Jla3ZQPHoy0QMTQQEFmJs3Ii5VGYlHGw2fnn7171Vffj 3qqbaPNULV5x5lS/kmi9n8ctImfu/TdDIezv/2gRc2Gu4I5OcMlTRcPViPt9mQbl 6vjsS/2pCtuuB1SRN4+qJpqHCSWGyAJDY14uNhgfxqPwC5z5YZp7NYnD1ZfCE2Vq EQp4Kijf8L8oeGPpkYqjLFHJgJBGr4AGiKYzx8ETV9MIGCsDsAsAeQYn9EFYtuOf qqS0itP+MtwEqS74zQ+leDrP6nPSr8wLpYVUo/R8pTv/0Q8nvM/nDShDjv6Etmkp XOZZ7ZJOO57exT6W2fpZt12T3N19lblKRC0YuJpWaw8RhAvAcXx7BgcEPRb9JVWk 6XvyJ+Tl3pgL6RXUSTIglRci6QnVOh7gIGb9m9LGqadOlSjcUmpcPcyGq0jsm6oJ nHdsF+ebaqB+LqapEv+TmN9b4CXVP2DoMSYfD+FffESaM99IapjyrsrfIpN2Gz7M Mlt7hiEt0V5OX88e8yGVSEVShQrJf0IJmK8T7ZFr0TuvrvRt67mIxY55sgarwuAG fivwqr2HwvnbXI1+nlXWQhDWykKQIw4QWEO0PsOPfULLB+eEog== =dmYY -----END PGP PUBLIC KEY BLOCK----- ``` # Swanky Documentation ## What is Swanky? Swanky is Galois’s open source suite of Rust libraries for secure computation. This all-in-one toolkit contains cryptographic components that academic, industry, or government users may need for a wide array of privacy-preserving tasks. Whether you are building a protocol using garbled circuits, experimenting with zero-knowledge proofs, or looking to use private set intersection to protect sensitive data, Swanky provides necessary primitives, eliminating the need to build everything from scratch. [View on GitHub](https://github.com/GaloisInc/swanky)
## Core Features and Capabilities * **All-in-One Toolkit:** Combines existing Galois diverse Zero Trust Computing technologies into one convenient package including zero knowledge (ZK) proof systems; garbled circuits; Oblivious Transfer (OT) and vector oblivious linear evaluation (VOLE), private set intersection (PSI); and core primitives, including finite fields, efficient random number generators, cross-platform SIMD support, and more. * **Professional Standards:** Existing frameworks are often academic in nature and not practical for adoption. Swanky aims to change the status quo by focusing on software quality assurance, usability, and secure hygiene. Our ultimate goal is a codebase where all cryptographic primitives are developed to professional software engineering standards, offering well-documented and consistent interfaces. * **Rust Benefits:** Swanky is written in Rust, which allows for benefits like memory safety and static analysis. Written correctly, Rust programs completely eliminate classes of vulnerability common in many programs written in languages like C or C++. With Rust, Swanky has a framework that is supportable, maintainable, and usable by both researchers and industry professionals. ## Open Source Swanky is an open source project, hosted on GitHub, licensed under an MIT license. The R\&D community, industry, and the public at large benefit when tools like Swanky are open sourced. In addition, open-source tools themselves benefit from and be independently verified by a broad, diverse user community. With this in mind, Galois has developed Swanky as an open source resource from the very beginning and kept it open for anyone to use and explore. [Swanky Repo](https://github.com/GaloisInc/swanky) You can also browse the Swanky documentation [here](https://galoisinc.galois.com/swanky). ## How can YOU use Swanky? While Swanky is open source and freely available, it’s important to note that it is complex enough that it requires expert knowledge to use to its full potential. Researchers and academics are, of course, welcome to experiment with this open source collection of libraries. However, businesses with secure computation needs but without expertise in secure multi-party techniques may benefit from working with us for ongoing support or to develop custom applications tailored to their needs. Importantly, Swanky is not a one-off build. Galois is actively adding new capabilities, and will continue to provide updates and support well into the future, along with roadmaps of upcoming capabilities. To learn more about how Swanky could serve your business needs or research goals, feel free to contact us at .
# C2Rust ## From C to Rust, to Better Rust Many of the most important systems in the world are written in inherently unsafe languages such as C, the memory-related vulnerabilities of which expose a significant attack surface for hackers. It would be beneficial to rewrite these languages in safe-by-design languages, such as Rust, but migration of a real system by hand is enormously expensive and time consuming. This is why, for more than a decade, [Galois](http://galois.com) and [Immunant](https://immunant.com/) have been developing **C2Rust, our automatic migration tool that is able to translate most C modules into semantically equivalent** [**Rust**](https://www.rust-lang.org/) **code.** *Click the link below to try C2Rust for yourself!*
C2Rust Demonstration →https://c2rust.com
Our original C2Rust transformed C code into unsafe, C-like Rust code. This is the first step of migration, but ultimately, we want Rust that is safe, performant, and idiomatic. The current state of the art is to run C2Rust, and then for an expert team to migrate the rest of the way. Immunant have done exactly this on the migration of the dav1d codec library to Rust. The next step, currently in active development, is to create an automated migration tool that can fully transform C code to safe, performant Rust. Even as the C2Rust continues to improve, it is already being widely used — for example, the popular serde\_yaml crate is just a wrapper around c2rust-transpiled code. No matter your current tech stack, there are effective ways to integrate C2Rust into your workflow. This project is available under the [BSD-3 license](https://github.com/immunant/c2rust/blob/master/LICENSE). ## Download C2Rust Source code and instructions are available in our [git repository](https://github.com/immunant/c2rust). ## Contact To report issues with the translation or tool, please use our [Issue Tracker →](https://github.com/immunant/c2rust/issues) For more information, email us at [info@c2rust.com →](mailto:info@c2rust.com) ***
# Documentation The [C2Rust manual](https://c2rust.com/manual) is available online and is our comprehensive documentation for using and developing C2Rust. ## Learn More More information about installing c2rust from [crates.io](https://crates.io/) is availble in this introductory blog post: [Introduction to C2Rust](https://immunant.com/blog/2019/08/introduction-to-c2rust/) Per Larsen recently presented a talk on C2Rust at RustConf detailing both our approach to translation as well as our *cross-checking* approach to testing the resulting translations. [RustConf 2018 - C2Rust: Migrating Legacy Code to Rust](https://www.youtube.com/watch?v=WEsR0Vv7jhg) Eric Mertens wrote a blog post describing some of the challenges we encountered during translation of C to Rust and how C2Rust tackles them. [C2Rust Challenges](https://galois.com/blog/2018/08/c2rust/) # FAQ ### Why isn't my type definition translated? Types that aren't used to generate code are pruned away. Try using your type in a function declaration. ### Why isn't *printf* available? You'll need to include headers to use functions from external libraries. ### Why was my function omitted? When the translator can't handle a translating a function for some reason it omits the implementation and prints the reason. This is configurable and visible when you're running the tool locally. Currently this web interface doesn't show warning messages generated during translation. ### What are the known limitations? We've captured many of the features we don't support on the [Known Limitations of Translation](https://github.com/immunant/c2rust/wiki/Known-Limitations-of-Translation) wiki page.