Slashdot Mirror
Cryptol, Language of Cryptography, Now Available To the Public
solweil writes to mention that Cryptol, a 'domain specific language for the design, implementation and verification of cryptographic algorithms,' is now available to the public. Cryptol was originally designed for the NSA. It allows for a quick evaluation and continued revisions, and is available for Linux, OS X, and Windows.
Second Post!
41R5T 3N6RI27ED P057 !
Having worked at the Agency I must say that the quality of the 'product' that they turn over to the public domain is second to none (well, except for that which they keep for themselves of course). They take a lot of heat at a leadership level, some warranted, some not. In the end, the caliber of the engineers, security professionals and JPG (just plain geeks) that work there is second to none. From SEL to crypto bake-offs to the submitter's topic, they've done a helluva lot of good for the community. Thanks guys! Now if they could just get 'Weed Man' to open an omelet shop out in town, all would be right with the world (inside joke, sorry).
So, wait, the NSA just released math?
Sounds more like a drug than a programming language.
Do you even lift?
These aren't the 'roids you're looking for.
Is there something intrinsic to cryptographic protocols that requires a timed release?
Doesn't it seem probable that anything created with an NSA tool will be more reversible with other NSA tools?
Those are my principles, and if you don't like them... well, I have others.
SRC="http://ad.doubleclick.net/adj/N763.no_url_specifiedOX2531/B3272816.16;sz=336x280;click=http://ad.doubleclick.net/click%3Bh=v8/37a2/3/0/%2a/z%3B210347091%3B0-0%3B1%3B13358338%3B255-0/0%3B29593640/29611519/1%3B%3B%7Eokv%3D%3Bpg%3Darticle%3Blogged_in%3D1%3Bdcopt%3Dist%3Btile%3D1%3Btpc%3Dit%3Btpc%3Ddevelopers%3Btpc%3Dprogramming%3Btpc%3Dsecurity%3Btpc%3Dtechnology%3B%7Esscs%3D%3f;ord=6242438?">
Looks like the Technocrat 'creeps' are already migrating to /.:
http://news.slashdot.org/article.pl?sid=08/12/26/1126256
Neat. There's some similarity to Matlab, and some to Renderman, and some of the syntax is borrowed from Haskell. The language is compilable to VHDL, so it's possible to generate hardware from the spec. The language is recursive and doesn't support iteration (there's no "for" statement) to make proof of correctness work easier.
This language might also be useful as a way to express compression algorithms. Reference implementations of the various "zip" algorithms in Cryptol would be useful, and ones for JPEG and MPEG compression, which are often implemented in hardware, even more useful. It's not clear how well Cryptol deals with memory-heavy problems like motion recognition or Hamming table building for compression, though.
Bruce Perens posts as an AC?!?!
Do you even lift?
These aren't the 'roids you're looking for.
Why would they release this? Don't get me wrong, I, personally, am all for donating to the community and further advancing technology as a species; however, why would the NSA deliver something to the public that would, in the long run, possibly make life harder on themselves by possibly furthering the advances of private encryption? I'm not trying to play Devil's Advocate, I just genuinely don't understand why they would (possibly) make life harder for themselves.
"The best way to accelerate a Macintosh is at 9.8m/sec^2" -Marcus Dolengo
At last, we now have a programming language that implements rot13() natively! Now my website's login authentication system will really fly...
FTFA:
"The open version does not compile to VHDL, C/C++, or Haskell, and does not produce the formal models used for equivalence checking."
So does this mean the open version (trial version) which we might have access to does not do much of what it is touted to be good for?
Just another advertisement for a commercial product methinks. Maybe cool, but still a slashvertisement.
- Toast
Use Cryptol + AJAX!
Clarification:
Cryptol, as I understand it, was developed by Galois (who, for some reason, is not mentioned in the summary) and not by the NSA. It would be interesting to know whether it was a joint decision between Galois and the NSA to release cryptol, or just Galois' decision alone.
Considering we paid for its development with public funds, it best not be 'commercially' released.
---- Booth was a patriot ----
So if someone used Galois to release a binary, and released the Cryptol source under the GPL, would the resulting binary be considered Free Software per the FSF's definition?
A casual perusal did not really confirm the connection between Galois.com and the NSA.
Google did not really help either:
http://www.google.com/search?hl=en&as_q=NSA&as_epq=&as_oq=&as_eq=&num=10&lr=&as_filetype=&ft=i&as_sitesearch=www.galois.com&as_qdr=all&as_rights=&as_occt=any&cr=&as_nlo=&as_nhi=&safe=on
http://www.google.com/search?q=NSA+Galois
Nothing in the world is more dangerous than sincere ignorance and conscientious stupidity.
Galois does high assurance computation for the NSA, and others. (Which is to say, the NSA expects Galois to do theorem proving on their code)
Does anybody have any good information about Cryptol? Is it a Haskell subset/extension? Most of what I know about Galois is in relation to Haskell.
After all, I am strangely colored.
Check yourself there. It takes longer to perform division on larger numbers (say O(ln(N)^2), though a lot of this depends on the algorithm). If you plan to do the sieve of eratosthenes as you describe (the hard way), that's going to be another O(n*ln(ln(N)) for a total of O(n*ln(N)^2*ln(ln(n))) for each factor.
The sort of numbers you are thinking about when you say that testing via division is O(1) with hardware are 64 bit integers. The sort of semi-primes used in cryptography are on the order of 512 bits, and so (by the formula above) would take roughly 147, 184, 841, 669, 860, 395, 336, 238, 071, 097, 320, 918, 206, 612, 375, 539, 181, 907, 207, 001, 765, 334, 079, 455, 842, 963, 079, 473, 553, 687, 769, 537, 122, 026, 054, 410, 625, 268, 901, 031, 540, 756, 829, 794, 467, 840, 000 times as long.
So if your computer took a nanosecond to solve a 64 bit case (making it faster than the fastest consumer system presently available), and you had a million of them, and all 6 billion people on Earth were your friends, and each of them had a million of these uber boxes as well, and you had a way to collaborate on the problem with no overhead, it would still take you roughly 1, 920, 658, 729, 429, 876, 148, 289, 055, 386, 140, 718, 898, 913, 520, 422, 922, 263, 604, 244, 594, 006, 798, 154, 722, 944, 671, 495, 344, 450, 391, 916, 549, 249, 431, 238 times the age of the universe to factor one such number.
That's why nobody does it that way, and why it's considered a hard problem even though it might sound easy.
-- MarkusQ
There's some documentation on Galois' web page. I looked at it once awhile back, and it seemed a lot like Haskell, but with extra syntax for doing common cryptographic operations.
Chapter 8 of the programming guide has example cryptol implementations of DES, RC5, and AES.
Galois.com: "Page not found." Cute. Yuk, yuk, I get it. No Such Company(tm).
As someone that's worked with Cryptol, I can tell you that it is indeed a very cool language. You can generate very efficient hardware off of a Cryptol spec, prove logical equivalence between two versions of an algorithm, and play with your specification interactively from a command line. There's even a startup called Signali that's been founded to expand the usage of Cryptol to the commercial sector and algorithms other than cryptography.
Ok, so Galois has decided that, given the depressed economy, a few extra potential customers might be a good idea. Cause what you get is just the concept of the language. Whatever your bright mind may decide to do with it will remain bottled up until you pay for the full COMMERCIAL product, since what you download for free just lets you see that "gee, whiz, this might work in the Real World when I pay for the whole shebang...". And, given the origins of the product, I'm pretty sure there will be a lot of caveats as to who's on the DOD/NSA/CIA worthy-of-using-cryptol list.
That wasn't intentional. I think I must not have enclosed the "a href" tag properly. Here, let me try again.
I assure you that there really is such a company; I have visited their offices on several occasions.
Yes, that program would be free but see "Free But Shackled - The Java Trap" for more on why this situation is not desirable.
Digital Citizen
Unlike New Coke and New Math, Math 2.0 is really, truly the future. For reals this time.
At first I thought that read New Coke and New Meth... that would be interesting. :)
$ root yum install libedit
Loaded plugins: refresh-packagekit
Setting up Install Process
Parsing package install arguments
Package libedit-2.11-1.20080712cvs.fc9.i386 already installed and latest version
Nothing to do
$ root rpm -i cryptol-academic-1.8.1-0.i386.rpm
error: Failed dependencies:
libedit.so is needed by cryptol-academic-1.8.1-0.i386
$ cat /etc/issue
Fedora release 9 (Sulphur)
Kernel \r on an \m (\l)
Next...
It's a commercial product. They want to cash in on it. Source and full implementation are not freely available.
IANAC (I am not a cryptographer.) but wouldn't this be a useful tool for criminals and terrorists? It would seem the height of folly to give such a tool away to them ... unless there was a way of mitigating it's usefulness.
There is no free lunch.
"Consensus" in science is _always_ a political construct.
Ok, there still seems to be confusion on it being "publicly" available. This is payware with a limited trial version. The headline is about that this advanced suite (I presume, I haven't used it myself) has become available *at all*. Previously, I presume, you could not just buy it. Of course, I also presume you could freely download it from some hacking site, but that's beside the point. Law only counts for law abiding citicens.
How sad that you choose to engage in name-calling instead of spelling out your apparent disagreement respectfully. Before you get into that, should you choose to explain your earlier statement, you should keep in mind the remarkable history of achievement and prescience Stallman shares with us. I don't seek perfection in anyone but I can't think of too many people who have given us all so much practical useful stuff and wisdom to think about. Specifcally, it's not every hacker who writes wildly popular licenses (GPL, LGPL), lots of software which is still immeasurably useful today (GDB, GCC, GNU Emacs, and so much more), and encourages us to keep in mind our freedoms to share and modify so that we can work with each other cooperatively and without foreseeable exploitation which pits us against our own work. Short-term and long-term that's impressive work even if you don't like his politics. Is it really that hard to be civil while expressing contrary views?
Digital Citizen
You don't need a crypto-language;
You can program encryption in everything from Assembly to Ruby.