The Challenge At Galois, we verify and assure complex critical systems. Autonomous vehicles are prime examples of complex systems which operate in uncertain and unstructured environments. Autonomous driving decisions use Deep Neural Networks (DNNs) which are data-driven and can react in unsafe ways when faced with out-of-distribution driving scenarios. Rigorously assuring the safety of these systems […]
Galois is open-sourcing MATE, a suite of tools for interactive program analysis with a focus on hunting for bugs in C and C++ code. MATE unifies application-specific and low-level vulnerability analysis using code property graphs (CPGs), enabling the discovery of highly application-specific vulnerabilities that depend on both implementation details and the high-level semantics of target […]
Conclusion You’ve now seen most of the essential features of cclyzer++. The next post will explore some more advanced topics and bring it all together with a larger example.
Galois has long been an advocate of utilizing formal approaches, such as mathematics, models, data, artificial intelligence and more, to build better systems. Galois had the privilege to continue this advocacy by supporting the Dayton Digital Transformation Summit, which took place from August 2 – 4, 2022, in partnership with the Air Force Digital Transformation […]
At the Mining Software Repositories (MSR2022) conference in May, we presented our LAGOON tool resulting from the DARPA SocialCyber AIE, and led a discussion session on reducing complexity of machine learning. LAGOON provides a comprehensive platform for analyzing and investigating open-source software (OSS) communities for potentially malicious contributors. This is accomplished by ingesting multiple types […]
We are pleased to announce the release of Crux 0.6. Crux is a tool for verifying programs containing inline specifications. Crux works with both C/C++ code (via Crux-LLVM) and Rust code (via Crux-MIR). This release brings a variety of improvements, including: Crux-LLVM now has improved support for LLVM debug metadata when the debug-intrinsics option is […]
We are pleased to announce the release of Cryptol 2.13.0. Cryptol is a language for writing and specifying cryptographic algorithms. This release brings a variety of improvements, including: The sortBy function is now implemented using merge sort instead of insertion sort. This improves both asymptotic and observed performance on sorting tasks. “Type mismatch” errors now […]
Cryptography continues to rapidly transform our world. It seems like every day there’s a new story about fully homomorphic encryption, blockchains, and how these technologies secure billions and even trillions of dollars in assets. We’ve talked about cryptographic algorithms and twice about cryptographic assurance. People who work with these concepts every day have been the […]
I’m excited to announce our paper “ANOSY: Approximated Knowledge Synthesis with Refinement Types for Declassification” has been accepted to PLDI 2022. Programs often need to reveal information about private or sensitive data. For example, consider an advertiser who wants to send an advertisement to users near a restaurant. To accomplish this, the advertiser could write […]
I first attended POPL, the ACM SIGPLAN Symposium on Principles of Programming Languages, in Rome, as a first-year grad student in 2013. It was my first real experience in the programming languages (PL) community. My undergraduate advisor presented a paper I had co-authored at a co-located workshop. I attended the programming languages mentoring workshop (PLMW), […]
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.