Viewing Results for Category: Domain Specific Languages (1 of 3 Pages)

SMACCMPilot: Open-Source Autopilot Software for UAVs

As part of DARPA’s High Assurance Cyber Military Systems (HACMS), Galois is building critical flight control software using new software methods for embedded systems programming. Recently, Signal Online reported an overview of the HACMS program. We’ve been working on the HACMS program for about a year and we’d like to share more details about open source work we’ve […]

Read More

High-Assurance Base64

Author: David Lazar Galois’ mission is improving the trustworthiness of critical systems. Trustworthiness is an inherent property of a system, but we need to produce evidence of its trustworthiness in order for people to make informed decisions. The evidence, and its presentation is a key part of what is often called an assurance case. The […]

Read More

SIMON and SPECK in Cryptol

Last week, the NSA published two families of lightweight block ciphers, SIMON and SPECK: http://eprint.iacr.org/2013/404 We’ve formally specified both ciphers in Cryptol: https://github.com/GaloisInc/cryptol-examples/tree/master/simon+speck The following sections explore some applications of our specifications. Parameters SIMON and SPECK are cipher families: each algorithm in the family offers different security and performance based on parameters such as block […]

Read More

ZUC in Cryptol

ZUC is a stream cipher that is proposed for inclusion in the “4G” mobile standard named LTE (Long Term Evolution), the future of secure GSM. The proposal is actually comprised several different algorithms: A stream cipher named ZUC, LTEencryption algorithm (128-EEA3), based on ZUC, LTEintegrity algorithm (128-EIA3), which is a hash function using ZUC as […]

Read More

Merging SMT solvers and programming languages

Galois is in the business of building trustworthy software. Such software will have well-defined behavior, and that behavior is assured in some way, whether via model checking, testing, or formal verification. SMT solvers — extensions to SAT solvers with support for variables of non-boolean type — offer powerful automation for solving a variety of assurance […]

Read More

Copilot and the Arduino

Copilot is an embedded domain-specific language designed by Galois, that allows you to generate assured, embedded C code from programs written essentially as Haskell lists (using Atom as a backend for the C code generation).  Lee Pike has written a tutorial on how to use Copilot to program an Arduino controller to play “Jingle Bells”. Read the full tutorial on […]

Read More

Building a business with Haskell: Case Studies: Cryptol, HaLVM and Copilot

During BelHac, the Ghent Haskell Hackathon in November, we took an afternoon session for a “Functional Programming in Industry” impromptu workshop. The following are slides I presented on Galois’ experience building a business using our functional programming expertise, in particular, Haskell. The talk describes three case studies where “functional thinking” helped shape the solution to […]

Read More

Tech Talk: Copilot: A Hard Real-Time Runtime Monitor

Galois is pleased to host the following tech talk. These talks are open to the interested public. Please join us!

title:
Copilot: A Hard Real-Time Runtime Monitor (slides, video)
speaker:
Lee Pike
time:
10:30am, Tuesday, 9 November 2010
location:
Galois Inc.421 SW 6th Ave. Suite 300, Portland, OR, USA(3rd floor of the Commonwealth building)
abstract:
We address the problem of runtime monitoring for hard real-time programs—a domain in which correctness is critical yet has largely been overlooked in the runtime monitoring community. We describe the challenges to runtime monitoring for this domain as well as an approach to satisfy the challenges. The core of our approach is a language and compiler called Copilot. Copilot is a stream-based dataflow language that generates small constant-time and constant-space C programs, implementing embedded monitors. Copilot also generates its own scheduler, obviating the need for an underlying real-time operating system. This talk will include fun pictures and videos.
bio:
Lee Pike has worked in Research & Development at Galois, Inc. since 2005. His primary area of research is dependable embedded systems, including both safety-critical and security-critical systems. Previously, he was a research scientist with the NASA Langley Formal Methods Group. He has a Ph.D in Computer Science from Indiana University. He has a Best Paper award from Formal Methods in Computer-Aided Design (FMCAD’2007), and service includes being on the program committees of FMCAD and Interactive Theorem Proving. His publications and other information can be found at http://www.cs.indiana.edu/~lepike.
Read More

Concurrent Orchestration in Haskell

John Launchbury presented the Orc language for concurrent scripting at the Haskell Workshop, 2010 in Baltimore.

Concurrent Orchestration in Haskell
John Launchbury
Trevor Elliott

The talk slides are available in PDF or online.

We present a concurrent scripting language embedded in Haskell, emulating the functionality of the Orc orchestration language by providing many-valued (real) non-determinism in the context of concurrent effects. We provide many examples of its use, as well as a brief description of how we use the embedded Orc DSL in practice. We describe the abstraction layers of the implementation, and use the fact that we have a layered approach to establish and demonstrate algebraic properties satisfied by the combinators.

Read More