Advance to content

Galois
Technology
Client Services
Company
Blog

Entries in the “Galois News” category

Galois, Inc. Wins Two Small Business Research Awards from Federal Agencies

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.

DHS Topic: Highly Scalable Identity Management Tools

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.

DOE Topic: Grid 2.0: Collaboration and Sharing on the Grid

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.

About Galois, Inc.

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)

Achronix and Signali: High-performance 128-bit AES cores for Speedster FGPAs

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.

Read the full story.

Posted in Galois News | Comments (0)

One Million Haskell Downloads…

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:

  • Total, and growing, Haskell source downloads
  • The most popular Haskell projects hosted on Hackage
  • The most popular development categories
  • The most popular methods for distributing Haskell source

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:

  • Monthly downloads per package (CSV, HTML)
  • Packages by download frequency (CSV, HTML)

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)

Signali: A Custom IP-Design Company

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)

Cryptol, the language of cryptography, now available

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)

Galois awarded NASA research contract

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)

Galois @ ICFP: See you there!

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)

Parsing the Linux kernel with Haskell: experience with Language.C

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

The bike commute challenge – status

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

Galois Open House

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