Viewing Results for "verification" (5 of 16 Pages)
Digital engineering (DE) is gaining momentum as the system engineering community matures practices and tooling. In its present avatar, DE workflows and tools rely on MBSE (Model-Based Systems Engineering) for developing and maintaining digital system artifacts and keeping these artifacts in sync during all phases of the system. This is presently achieved via descriptive models […]
In prior posts, we’ve discussed techniques and benefits of digital engineering (DE) applied to system design, in particular hardware and software for cyber-physical systems (computer systems that interact with the real world). In this post we’ll simultaneously go big and small to present a case study in how formal methods + models can enable us […]
Software supply chain attacks are on the rise, increasing a staggering 742% per year on average since 2019. Sometimes called “third party attacks,” these cyberattacks infiltrate third party or open source software libraries with malicious code, infecting vendors and components along the software supply chain. These days, any given software artifact may depend on hundreds […]
In the world of cyber physical systems, the aim of Digital Engineering (DE) is to speed up the development process while simultaneously improving security, reliability, safety and performance. The core mechanism enabling this outcome is a refinement based design and implementation process whereby high-level requirements and reference architectures are refined into low-level requirements and system […]
Abstract: Low-level, pointer-manipulating programs are tricky to write and devilishly hard to verify, requiring complex spatial program logics to reason about heap updates. Recent systems like Prusti and Creusot take advantage of Rust ownership mechanisms to shield the programmer from some spatial assertions, allowing them to only write pure, first-order logic specifications which can be […]
Thus far in our ongoing series on artificial intelligence we’ve spoken in depth on questions of trust, human perception, and limitations of generative models. We have focused specifically on large language models (LLMs), due in part to their recent successes and media attention. We’ve explored questions of data, testing, and broad model implications. However, LLMs […]
Overview We have added support for semi-automated proof assistance and repair to Crux, Galois’s symbolic testing tool for C/C++ and Rust. These new capabilities build on support for logical abduction provided by the cvc5 SMT solver that suggests possible facts for failed proof goals, that, when assumed, make the proof goals provable. This feature can […]
2022 wasn’t a return to pre-pandemic times, but we’ll call it a “return to almost-normal.” At Galois, we continued a hybrid model of in-person and virtual collaboration. We also added several members to our team, including the acquisition of Adventium Labs! (More on that below.) Throughout the year, we made considerable progress applying our efforts […]
Abstract: Since 2016, various members of Project Everest have been busy verifying layer after layer of critical software. We started with cryptographic primitives, moved on to high-level stateful APIs, followed by protocols, handshake state machines, and high-level defensive APIs complete with proofs of security in the Dolev-Yao symbolic model. In our most recent work, we […]
We are pleased to announce that Galois is open-sourcing cclyzer++, a new pointer analysis for languages that compile to LLVM, including C and C++. Pointer analysis is a foundational static analysis with applications to the problems of program optimization, verification, bug finding, and many others. At Galois, we designed cclyzer++ with two main use cases […]
We take pride in personally connecting with all interested partners, collaborators and potential clients. Please email us with a brief description of how you would like to be connected with Galois and we will do our best to respond within one business day.