CVE-2024-55581
When AdaCore Ada Web Server 25.0.0 is linked with GnuTLS, the default behaviour of AWS.Client is vulnerable to a man-in-the-middle attack because of lack of verification of an HTTPS server’s certificate (unless the using program specifies a TLS configuration).
That reminds me, I’d like to do a Ada/SPARK TLS implementation… but the best way to do that is an Ada/SPARK proved implementation of ASN.1. (The security certificate is, itself, an ASN.1 object, encoded with BER, if memory serves.)
I take my hat off. ASN.1 is sheer horror. Though I do not understand the problem, if client allows desired settings just do it.
There’s asn1scc compiler that generates SPARK code.
I’ve been working on that here if you’re interested: GitHub - docandrew/SPARKx509: Verified library for X.509 certificates. I’m not convinced my approach is the best way about it but I can do some basic certificate parsing with it.
I took a look at this tool, unfortunately is isn’t capable of handling many of the datatypes used in the x509 RFCs.
I think that’s backwards from what I was saying: implement ASN.1 in Ada/SPARK, not use ASN.1 to produce Ada/SPARK.
Hence why (in my estimation) it would be better to implement ASN.1 itself within Ada/SPARK: establishing the data-structures (i.e. the meta-object system), and then implementing the serialization/deserialization algorithms: going about this way, since you get the [meta]objects up and proven, then the production (stream-in & stream-out) of those objects proven, you would then have a system where X.509 certification is merely (a) defining the structure object data-structure, & (b) enforcing any additional constraints. (Also, this route gives you a solid, proven ASN.1 implementation that you can use for all other ASN.1-using projects/systems.)
That’s the benefit of the method; the drawback is that it is the up-front implementation of the ASN.1 standard, all of it, which is a lot of work.
Cool!
I’m glad you have some initial results; it’s really satisfying to see progress sometimes.
I can’t promise I’ll get around to looking/poking any time soon, but I did want to give a little encouragement: Good job!
And it’s ok even if your current design isn’t the best, so long as you are learning. (That’s the point of experimenting.) It’s the engineering of a solution that needs to be “the best”, so you can allow yourself to “flail” a bit in your explorations.
Simple Components contains a full Ada implementation of ASN.1. X.509 certificates are provided as one of examples. See.