Ada version of curl?

General
1

I have just read this post: Death by a thousand slops

Even though the topic is more about fake bugs (as I understand it), the kind of vulnerabilities mentioned (mostly buffer overflows) hint at (or even scream for) a nice project idea: an Ada version of curl:

  • Name: Aurel
  • Primary API: in Ada
  • C API for compatibility and replacing curl

The most possible parts would be made with SPARK.
It could be a nice advertisement for Ada/SPARK (my impression is that curl is a very “visible” / pivotal software).

But perhaps such a project already exists?

1 Like
2

I never used curl. But if you look at the network clients landscape then you find in the same category of tools:

  • wget
  • sftp
  • yt-dlp
  • WinSCP
  • MQTT explorer

As a side note, I do not like command-line utilities in general. Either GUI or a library for me.

P.S. I do not think SPARK is needed to fight buffer overrun. What I do in network clients/servers is sticking to Stream element array and String, arena pools and the standard Ada API approach: buffer + last. All buffer sizes specified in advance. It is 100% bulletproof, IMO.

3

This is misguided: do everything without respect to C first… then shim in a C compatibility module for export.

1 Like
4

curl does both: command-line and library.

5

Well, if the Ada API relies on indefinite types (unbounded arrays, tagged types) and/or generics that would be very difficult. You better plan C API in advance, if you want them.

Furthermore, C will be involved anyway in the form of OpenSSL and/or GNUTLS. I doubt the author plans to reimplement them. Which I would welcome, of course.

To the point. There was Ada Crypto Library project, which unfortunately is no more supported.

I studied it a lot with regard of primality and arbitrary precision numbers, when I implemented these the Simple Components. It well written, understandable and contains many encryption algorithms which might be useful. I too implemented ChaCah20 and AED and have an Ada ASN.1 implementation (you need it for keys and certificates).

Anyway if anybody is brave (or stupid :grinning:) enough to give an Ada TLS a try, let it be known!

6

How about SparkNaCl?

I have never used it, but the README contains this text:

22nd June 2022

A bunch of updates have been merged to the master branch recently. Specifically:

  • Jon Andrew has kindly contributed implementations of the ChaCha20 stream cipher (in SPARKNaCl.Stream), SHA-256 (in SPARKNaCl.Hashing), SHA-256-based HMAC and HKDF algorithms (in SPARKNaCl.MAC and SPARKNaCl.HKDF respectively) and the an AEAD algorithm (RFC 8439) using ChaCha20 and Poly1305 (in SPARKNaCl.SecretBox), plus additional test cases and clean proofs. These additions take the library well beyond the original specification of NaCl, and move towards supporting TLS 1.3.
7

Yes it’s certainly possible and a verified TLS library in SPARK is a long-term goal (maybe dream) of mine.

SPARKNaCl has all the primitives you’d need, it recently added more SHA functions to make the other TLS 1.3 cipher suites possible.

I have a proof-of-concept for the handshakes here: SPARKTLS/src/tls.adb at fd58359697d4d086738f0e1d2bf058027f7819ff · docandrew/SPARKTLS · GitHub

I started on my own x509 library GitHub - docandrew/SPARKx509: Verified library for X.509 certificates but it’s pretty rough, Dmitry’s might be a better starting point. I think RecordFlux’s verified record parsers would also be a really great tool to try to apply to the project.

The building blocks are all there! It just needs a hero with more mental horsepower and/or free time than I have :slightly_smiling_face:

6 Likes