June 29th, 2009 by Galois
Galois, Inc., a Portland, Oregon research and development company, has been awarded two Phase I Small Business Innovative Research contracts. Galois will be engaging with the Department of Energy and the Department of Homeland Security on innovative technology solutions.
Galois has been granted a Phase I SBIR from the Department of Homeland Security to develop a reusable identity management metasystem which will be designed foundationally to support government certification for deployment across agency boundaries, focusing on open standards, secure development, and a cross-domain design.
The Department of Homeland Security’s charter has a fundamental requirement to collaborate with other government agencies. Secure collaboration on this scale requires strong identity management which can “vouch for” DHS personnel working with other agencies and makes it possible to provide DHS resources to individuals in other agencies whose work requires it.
Anticipated Benefits: This work will provide an opportunity to deploy standard trusted components in a variety of agencies, each of which can continue to maintain its own method of managing identity and authorization. Agencies can share information based on this layer, which will evolve to support a wide variety of needs.
Potential commercial applications: Compliance with government standards of trustworthiness in software used for critical purposes, along with a user-centric approach to identity management, can enable Internet users to merge their many usernames and passwords, allow critical transactions to be executed with a higher degree of trust, and help bring about an environment where e-voting increases voters’ trust in the validity of the outcome of elections.
Galois has been granted a Phase I SBIR from the Department of Energy to implement a Web 2.0 collaboration system based on Grid technologies. Galois’ system will allow dispersed scientific teams to collaborate effectively on large amounts of data produced by collections of networked computers.
Grid computing makes accessible significant computational and data resources to distributed teams of scientific researchers. In doing so, it also poses a challenge: How do distributed teams collaborate effectively with these resources?
The problem is determining how best to apply social and collaboration software techniques to improve the efficiency of collaboration between distributed teams working on grid systems.
Potential Commercial Applications: Grid computing is inherently social in the sense of involving multiple, loosely connected parties. Social collaboration in the area of large datasets is relevant to industrial and academic scientists.
Galois is a research and development company with a strong drive to transition technology from research into practice in the commercial and government sphere. Located in downtown Portland, Galois is a company of around 35 employees, including software developers, project managers, and business development personnel. Galois has experience in programming language design and compiler implementation, secure web application development, secure operating system development, and several other fields. Since its founding in 1999, Galois has been funded for R&D by members of the Intelligence Community and the DoD. Read more about Galois’ research and technology on their web site: www.galois.com.
Posted in Galois News, Technology | Comments (0)
May 7th, 2009 by donstewart
Achronix Semiconductor, maker of the world’s fastest FPGAs, today announced (.pdf) the availability of new, high-performance AES IP cores for its SpeedsterTM 1.5 GHz family FPGAs.
These high-performance 128-bit key size AES core are targeted at 10 Gbps, 40 Gbps, and 100 Gbps applications have been designed and built by Signali, a Galois spinoff focusing on custom cores targetting computationally intensive algorithms, fixed-function DSP and cryptographic applications. Signali uses their Quattro™ compiler suite to transform high-level descriptions of data-intensive functions, such as AES into high-performance RTL.
Posted in Galois News | Comments (0)
March 23rd, 2009 by admin

Galois engineers write a lot of Haskell (in fact, our tech catalogue is built pretty much entirely on it). We find we’re able to build systems faster, with fewer errors, and in turn are able to apply techniques to increase assurance, helping us deliver value to our clients. We’ve successfully engineered large systems in the language for nearly a decade.
We also use and write a lot of open source Haskell code.
Since 2004 we’ve been investing in improving packaging and distribution infrastructure for Haskell code, and since 2007 Galois has been hosting hackage.haskell.org: the central online database of open source Haskell libraries and applications. These packages are built via Cabal (dreamed up by Galois’ own Isaac Potoczny-Jones), and distributed via cabal-install. Hackage now hosts more than 1100 released libraries and tools, and has been growing rapidly (and, incidentally, Galois employees have released or been significant contributors to just shy of 10% of all Hackage projects).
We’ve wondered for a while now just how busy Hackage was becoming, and in turn, what other interesting information about Haskell were buried in the Hackage logs. This post answers those questions for the first time.
We’ll see:
And speculate a little on where Hackage is heading.
Background
We’ve known for a while that uploads to Hackage were growing. You might have seen this graph elsewhere (it’s derivable from the RSS logs of package uploads):
There’s a pretty clear trend upwards. Average daily Hackage releases have increased 4-fold since Hackage was launched, and it’s now averaging 10 packages a day released. The question is: was anyone using this code?
Measuring Downloads
To measure downloads, we processed the apache logs for Hackage going back to its launch (incidentally, the log processing script – in Haskell of course – uses the Haskell zlib, bytestring, filepath, containers, bytestring-csv libraries). This generates a two dimensional map of downloads per project, per month. (You can find links to the raw data at the end of the article).
We can now play with the data to see some interesting trends.
Some cautionary notes interpreting this data: we only process Hackage package downloads (i.e. “GET binary-0.5..tar.gz” requests). We are only able to measure source downloads – that is, someone downloads a package they will build from source, with GHC. We cannot measure downloads from open source mirrors (such as those provided by the major unix distributions), nor can we measure users of binary packages (such as on Debian, Ubuntu or Fedora), nor can we measure downloads of packages not hosted on Hackage (such as gtk2hs, pugs, darcs or ghc). So this doesn’t represent all Haskell downloads, only downloads of source packages.
We have complete data for Hackage, from the initial alpha tests in July 2006, through to launch in January 2007, until March 2009.
Total Downloads
To begin with, here’s the cumulative downloads from Hackage, over time:
As you can see, we’re just shy of 900 thousand package downloads, and from January 2008 to December 2008 – the first complete year of live operation – there were 500 thousand downloads, with a further 150 thousand downloads in the first 2 months of 2009.
To visualize the growth trend, here is the same cumulative download line on a logarithmic scale:
In the alpha-testing period from July 2006 to July 2007, downloads grew exponentially (4 orders of magnitude in 4 quarters) as existing developers started to use the system. Since the middle of 2007, the rate of growth has slowed, increasing by an order of magnitude in a 15 month period.
Hackage is on target to reach its 1 millionth download next month. We’ll have a party.
Downloads by Month
Next up is the downloads per month, over time. I dropped a bezier curve on top to give a sense of the trend. As we only have partial data for March 2009, I’m excluding that. This graph essentially confirms the same trend as we see in the cumulative graphs. Interestingly, download spikes roughly correspond with upload spikes in our first graph (presumably as people scramble to get the new code).
Hackage is currently seeing 100 package downloads an hour, and that value has been doubling every 4 months for the past year and a half.
Package Popularity
Besides overall downloads, there’s a wealth of per-package information. In the following graphs we extract total downloads for each package (ignoring version numbers).
The popularity graph displays a classic “long tail“, where the download frequency of any package is inversely proportional to its rank in the frequency table.
This suggests that a good interface to a large Hackage database should behave something like the “long tail” sites like Amazon – where we rely on recommendations and other interlinking to ensure visibility of projects in the tail.
The frequency of downloads is even more visible on a double log scale, where the popularity pretty much matches Zipf’s law:
The download frequency doesn’t quite match the classic distribution at the top and tail of the curve. There are two reasons for this (and maybe other factors at play). Firstly, the tail of the curve drops off, as the bottom 10% of popular packages tend to be the newest packages, and so are unde-represented in the “market”.
The other interesting part of the popularity curve is at the top. The top 10 to 50 packages are, to varying degrees, less popular than we might predict. Why is this?
The Distribution Effect
Remember that Hackage is a source-only repository. So it is of primary interest to developers. As a Haskell package becomes more popular, it tends to get picked up by Linux and BSD distributions such as Debian or Ubuntu (and also distributed in binary form for Mac and Windows), removing the need to download the source. Popular packages are doomed to become less popular in source form if the distributions are doing their work!
This is particularly apparent for libraries distributed with GHC (the “extra libs”). Libraries such as containers, arrays, bytestring, parsec and network rarely need to be downloaded in source form, as they’re bundled with GHC forming a platform base. They should thus be under-repesented in source downloads.
You can see this “distribution effect” in this overlay of xmonad and its Debian package installs where source installs decline dramatically as soon as the binary packaging takes off.
Popular packages are doomed to be distributed through other channels.
Most popular packages
And here – for the first time – are the per-package popularity statistics for Hackage. First, the top 25 packages sorted by their cumulative total downloads. Executable applications are marked in blue.
| 1 | xmonad | 35428 |
| 2 | HTTP | 26203 |
| 3 | zlib | 24431 |
| 4 | Cabal | 23691 |
| 5 | X11 | 21563 |
| 6 | binary | 15752 |
| 7 | utf8-string | 12633 |
| 8 | mtl | 12517 |
| 9 | cabal-install | 12274 |
| 10 | regex-posix | 11351 |
| 11 | X11-extras | 10509 |
| 12 | xmonad-contrib | 9794 |
| 13 | haddock | 9209 |
| 14 | parsec | 8468 |
| 15 | bytestring | 7473 |
| 16 | regex-base | 7438 |
| 17 | HaXml | 6307 |
| 18 | network | 6285 |
| 19 | xmobar | 6272 |
| 20 | yi | 6268 |
| 21 | hscolour | 6264 |
| 22 | QuickCheck | 5697 |
| 23 | hslogger | 5434 |
| 24 | regex-compat | 5266 |
| 25 | ghc-paths | 4653 |
And the next 75 Haskell packages, in order:
filepath, X11-xft, alex, happy, vty, cgi, terminfo, unix, GLUT, chunks, fingertree, OpenGL, time, pureMD5, regex-tdfa, xhtml, bzlib, Crypto, syb-with-class, hxt, tagsoup, HDBC, MissingH, SDL, haskell-src-exts, plugins, Stream, frag, curl, pcre-light, unix-compat, uniplate, wxcore, hinstaller, stm, html, Diff, polyparse, leksah, HUnit, hmp3, haskell-src, RJson, fastcgi, pandoc, arrows, YamlReference, parsedate, HGL, GLFW, process, extensible-exceptions, zip-archive, iconv, HDBC-sqlite3, TypeCompose, cpphs, hmatrix, HPDF, HAppS-Server, haskell98, hspread, HAppS-Util, rosezipper, gd, dlist, array, yi-gtk, haskeline, HStringTemplate, HAppS-Data, fgl, haskelldb, xml, cabal-rpm
Congratulations to authors of these packages – you made the top 10% most popular releases.
Most Popular Downloads in February
The previous table looked at the cumulative most popular projects. But that doesn’t necessarily reflect what is popular at the moment to download in source form. This table compares January downloads against February downloads, for the top 25 packages in Feburary:
| Package | Downloads | Rank Change |
| HTTP | 2926 | |
| zlib | 2345 | |
| Cabal | 2148 | |
| cabal-install | 1490 | |
| utf8-string | 1352 | |
| xmonad | 1280 | |
| binary | 1174 | |
| regex-posix | 901 | +8 |
| parsec | 842 | +2 |
| X11 | 834 | -1 |
| xmonad-contrib | 754 | +1 |
| hscolour | 739 | -2 |
| terminfo | 713 | +1 |
| haddock | 669 | -6 |
| ghc-paths | 630 | +2 |
| HaXml | 600 | +12 |
| extensible-exceptions | 596 | +16 |
| QuickCheck | 584 | +9 |
| regex-base | 558 | -4 |
| time | 529 | -1 |
| darcs | 501 | 1 |
| leksah | 500 | +18 |
| regex-tdfa | 496 | +24 |
| hslogger | 441 | -2 |
Most popular applications
The 25 most popular Haskell applications hosted on Hackage, to download in source form are:
xmonad, cabal-install, haddock, xmobar, yi, hscolour, alex, happy, frag, leksah, hmp3, pandoc, cpphs, cabal-rpm, darcs, c2hs, hoogle, lambdabot, cabal2arch, hpodder, monadius, lhs2tex, mkcabal, pugs, ghc-core
Note pugs and darcs have been primarily distributed separately to Hackage, until recently.
Most popular libraries by category
We can also determine the most popular libraries and tools in each semantic category on Hackage:
| Task | Library | Downloads |
| Client-side HTTP | HTTP | 26203 |
| Database | HDBC | 3098 |
| XML | HaXml | 6307 |
| Control | mtl | 12517 |
| Parsing | parsec | 8468 |
| Binary Parsing | binary | 15752 |
| Logging | hscolour | 6264 |
| Testing | QuickCheck | 5697 |
| Regex | regex-base + regex-posix | 7438 |
| Lexing | alex | 4360 |
| Codec | zlib | 24431 |
| Unicode IO | utf8-string | 12633 |
| Sockets | network | 6285 |
| Build System | Cabal | 23691 |
| Documentation | haddock | 9209 |
| Syntax | hscolour | 6264 |
| 3D Graphics | GLUT + OpenGL | 7345 |
| 2D Graphics | SDL * | 3016 |
| Hashing | pureMD5 | 3460 |
| HTML | xhtml | 3391 |
| Cryptography | Crypto | 3243 |
| Generics | syb-with-class | 3230 |
| IDE | leksah | 2408 |
| JSON | RJson | 2222 |
| Markup | pandoc | 2210 |
| Numerics | hmatrix | 1844 |
| Web Framework | HAppS-Server * | 1759 |
| Graphs | fgl | 1658 |
| Parallelism | parallel | 1370 |
| Charting | chart | 1300 |
| Code generation | llvm | 970 |
| RSS | feed | 726 |
| Wiki | gitit | 759 |
Note that SDL is represented here as gtk2hs (which provides many cairo-based 2D graphics functions) isn’t distributed on Hackage. Also, HAppS-Server has been superceded by happstack.
Honourable mentions
These packages didn’t quite take first place, but still have significant user support. I include happstack, although it is only a month old, as it replaces the previously popular HAppS-Server.
| Parsing | happy, polyparse | 6685 |
| Regex | Regex-tdfa, regexpr, pcre-light | 8791 |
| Codec | bzlib | 3275 |
| XML | hxt, xml | 4871 |
| HTML | tagsoup | 3141 |
| Client-side HTTP | curl | 2678 |
| Generics | uniplate | 2675 |
| 2D Graphics | wxcore | 2601 |
| Testing | HUnit | 2325 |
| Database | haskelldb, hsql | 3164 |
| Network | Network-bytestring | 1210 |
| Control | monadLib | 1081 |
| Web Framework | happstack | 549 |
Future
Finally, we can speculate on what would happen if the current download growth rate continued for a couple more years (projecting forward 18 months, using the trend of the last 18). We’d reach a cumulative total of 10 million source downloads around the end of 2010 (continuing the order of magnitude growth of the last 18 months).
Of course, a lot is unknown in this scenario. If everyone starts installing all their code via cabal-install, downloads will rocket, as does increasing reuse, by using more libraries.
However, if the top Haskell applications and libraries become an order of magnitude more popular, the distros will take them up, slowing growth. Growth will also slow if we run out of resources in some form or another: no more easy libraries to bind to, for example, just as we ran out of existing things to cabalize in 2007.
Get the data yourself
You can play with the data set yourself here:
You can also get the full data in a sqlite database, courtesy of mmorrow on #haskell.
Posted in Community, Cryptography, Functional Programming, Galois News, Haskell, Open Source | Comments (8)
January 13th, 2009 by john
Signali Corp is the latest technology commercialization spinout from Galois, chartered with commercialization of hardware IP core design technology aimed at the FPGA and ASIC markets. Engineers at Galois and Signali have used the proprietary technology to deliver to government prime contractors the highest performing FPGA implementations in the world for a set of common cryptographic algorithms.
With this technology, Signali is well-placed to make a significant impact on the IP core market with their ability to re-tune their cores to meet the customer’s design constraints, whether speed, or power, or area. The technology is especially well suited for optimizing hardware designs of computationally complex functions such as those common in digital signal processing and cryptographic systems.
Galois enlisted the experience of Brian Moore, a seasoned design engineer and lab director from Intel, to lead Signali. Moore brings over 25 years of experience in the semiconductor and energy research industries. Galois co-founder Jeff Lewis, is leading the technology development as Chief Technology Officer. Signali is currently co-located with Galois in the historic Commonwealth Building in downtown Portland, Oregon.
The company is engaged with Achronix Semiconductor to develop a portfolio of very high performance IP cores for their next-generation FPGAs. Sample performance and utilization numbers for IP cores running on the Achronix Speedster FPGA can be found on the Signali website.
Posted in Galois News, Technology | Comments (0)
December 24th, 2008 by magnus
Galois is pleased to announce that Cryptol, the language of cryptography, is now available to the public!
Cryptol is a domain specific language for the design, implementation and verification of cryptographic algorithms, developed over the past decade by Galois for the United States National Security Agency. It has been used successfully in a number of projects, and is also in use at Rockwell Collins, Inc.
Domain-specific languages (DSLs) allow subject-matter experts to design solutions in using familiar concepts and constructs. Cryptol, as a DSL, allows domain experts in cryptography to design and implement cryptographic algorithms with a high degree of assurance in the correctness of their design, and at the same time, producing a high performance implementation of their algorithms.
Cryptol allows a cryptographer to:
■ Create a reference specification and associated formal model.
■ Test the specification against published test vectors and formal assertions about state.
■ Quickly refine the specification, in Cryptol, to one or more implementations, trading off space, time, and other performance metrics.
■ Compile the implementation for multiple targets, including: C/C++, Haskell, and VHDL/Verilog.
■ Equivalence check an implementation against the reference specification, including implementations not produced by Cryptol.
The Cryptol site has further documentation and the full language specification.
In this release, Galois has made a implementation of the Cryptol language available free of charge for non-commercial uses.
The trial version is available for Linux, MacOS, and Windows installations and can be downloaded at the Cryptol site. The trial version is meant for language exploration. It includes a Cryptol interpreter with QuickCheck capabilities, documentation, and examples. The open version does not compile to VHDL, C/C++, or Haskell, and does not produce the formal models used for equivalence checking.
Cryptol is implemented in Haskell.
Contact Galois to obtain a full-featured version for evaluation.
Posted in Cryptography, Galois News | Comments (15)
November 11th, 2008 by Lee Pike
NASA has awarded Galois, Inc. together with the National Institute of Aerospace (NIA), a research contract to investigate monitor synthesis for software health management (here is NASA’s press release). The research team includes myself, Lee Pike as the Principal Investigator, Cesar Munoz as the Co-PI (NIA), and Alwyn Goodloe as a Research Scientist (NIA). The award runs through the end of 2011, and we are investigating the formal synthesis of online monitors from requirements specifications. The research will focus on safety properties and real-time properties of distributed systems. Here are some slides I gave as part of an invited panel kicking off the project, and here’s the press release from Reuters. If you’re interested in finding out more about the research or are interested in collaborating, don’t hesitate to contact me, or leave a comment!
Posted in Formal Methods, Galois News, Technology | Comments (0)
September 19th, 2008 by donstewart
ICFP is next week, and as usual, Galois will be involved, sponsoring workshops, chairing sessions, presenting papers, and generally talking to people about functional programming and the future. We’re particularly excited about the expanded Haskell Symposium, the line-up for the Commercial Users of Functional Programming, and the all-new DEFUN developer tracks on functional programming (watch Oleg hack live!).
If you want to catch up, keep an eye out for Andy, Don, Eric, Iavor, Joe, Joel, John, Levent, Magnus and Trevor, or follow us on Twitter. Happy hacking!
Posted in Community, Functional Programming, Galois News | Comments (0)
September 17th, 2008 by Aaron Tomb
At Galois, Aaron Tomb has been experimenting with the new Haskell Language.C libraries recently (a Summer of Code project by Benedikt Huber, mentored by a Galois engineer, Iavor Diatchki), and he’s been impressed by what it can do. Here are his thoughts on parsing the Linux kernel with Haskell, with an eye to future static analysis work:
My interest in the library is for use in static analysis of very large bodies of legacy C code, which means two issues matter a lot to me: 1) rock-solid support for all of GCC’s numerous extensions, and 2) speed. I have used CIL, and tools based on CIL in the past, but have been disappointed with its speed.
As a simple scalability and robustness experiment, I decided to see how well Language.C would do on the Linux source tree. It doesn’t yet have an integrated preprocessor (depending on GCC’s for now), but I happened to have an already-preprocessed set of sources for Linux 2.6.24.3 sitting around (configured with defconfig).
Could Language.C handle the Linux kernel?
I wrote a little wrapper around the C parser to essentially just syntax-check all of the code.
import Language.C
import Language.C.System.GCC
import System.Environment
process :: String -> IO ()
process file = do putStr file
stream <- readInputStream file
putStr (take (20 - length file) $ repeat ' ')
either print
(const $ putStrLn "Pass")
(parseC stream nopos)
main :: IO ()
main = do
files <- getArgs
mapM_ process files
It prints the filename followed by “Pass” if the parse succeeds, or details about a syntax error if the parse fails. When I ran this on the Linux code mentioned above, I was amazed to find that it processed it all successfully! All 18 million lines of pre-processed source without a hitch.
Since I also care about speed, I wanted to compare it with GCC. GCC has a handy flag, -fsyntax-only, which tells it to just check the syntax of the input file and quit. I ran both the Language.C wrapper
(compiled with GHC 6.8.3 and the -O2 option) and GCC on all that code, on a 2.2GHz/4GB MacBook Pro. The result: Language.C parsed all of the code in about 6 minutes, while GCC managed it in a little over 2. GCC is still faster, but I’m happy to take a 3x speed hit for the benefit of being able to write all the subsequent analysis in Haskell.
The following table shows the precise time and memory statistics for Langugage.C and GCC, both on the entire source collection and on the single largest file in the tree, bnx2.i, the driver for the Broadcom NetXtreme II network adapter. For the Language.C tests, I compared the performance when the garbage collector used 2 generations (the default) to 4 generations (specified with the +RTS -G4 option). Increasing the number of generations helped slightly.
| User Time | System Time | Memory Use | |
|---|---|---|---|
| L.C, all | 5:59 | 0:09 | 144MB |
| L.C, all, -G4 | 5:27 | 0:08 | 131MB |
| L.C, bnx2.i | 0:02.15 | 0:01.89 | 133MB |
| L.C, bnx2.i, -G4 | 0:01.96 | 0:01.76 | 85MB |
| gcc, all | 2:02 | 0:17 | ???? |
| gcc, bnx2.i | 0:00.56 | 0:00.07 | 33MB |
Posted in Functional Programming, Galois News, Haskell, Open Source | Comments Off
September 14th, 2008 by dylan
The Bike Commute Challenge is a wonderful Oregon tradition that Galois has participated in for the past 3 years. This year was a bit disruptive for Galois commuters, because we moved offices from Beaverton to downtown Portland. I think quite a few West-siders haven’t yet figured out the best way to get downtown by bike. Nevertheless, we’re holding steady at an overall 15% commute rate, with a few folks standing out from the crowd: Sigbjorn Finne at 360 miles and Paul Heinlein at 250 miles.
The challenge web site has had a few ups and downs (er, mostly downs), but it seems to be back on-line, so I’m hoping folks are able to log their trips without troubles. One weird thing is I think they’re miscomputing the commute rate – it says Paul and Sigbjorn are around 80%, but I’m pretty sure they’re both at 100%, so perhaps there are still a few kinks left to work out. (and once they are worked out, I suspect our overall rate will be well-above 15%)
Anyone reading this, please commend any of your bike-commuting colleagues, and I’ll take this opportunity to thank everyone for participating (Galwegians and everyone else!)
Posted in Community, Galois News | Comments Off
September 2nd, 2008 by Andy Adams-Moran

Please join us for an open house to celebrate our new office space in downtown Portland’s historic Commonwealth Building. Located on SW 6th Avenue between Stark and Washington streets, we’re easily accessible via MAX or TriMet buses. We’re up on the third floor.
Parking will also be available in the Alder Street Star Park parking garage located at 615 SW Alder, just one block from our building; validation will be provided at the event.
| What: | Galois Open House | |
| When: | Thursday, September 18 | |
| Time: | 4:00 pm – 6:00 pm | |
| Where: | The Commonwealth Building 421 SW Sixth Ave., Ste. 300 |
RSVP: Anne Marie @ ph. 503.626.6616, x153 or email anne at galois.com
Posted in Galois News | Comments Off
©2000–2010 Galois, Inc. All rights reserved. Terms of use. Contact Us