Re: ANN: Ada/SPARK ASN.1 implementation version 0.0.01

[ttsiodras@gmail.com]

On Monday, August 1, 2016 at 10:15:23 AM UTC+2, Shark8 wrote:
> I'm making public my ASN.1 project which aims to be a verified implementation of ASN.1, which is used in security-certificates, which is hopefully the first step in a verified-TLS/-TLS -- the project also aims to be [directly] usable in DSA projects.
> 
> As of 0.0.01 the only portion implemented is a pure big-number package, and another currently shared-passive unit for usability. 
> 
> I would certainly appropriate comments, criticism, and most especially contributions.

I am not sure if it can be used with the TLS ASN.1 grammar - but I think it's worth checking out our own open-source ASN.1 compiler, targetting both C and Spark/Ada (developed under the auspices of the European Space Agency, so targeting the same kind of safety-critical targets you probably have in mind).

The compiler is here: 

    https://github.com/ttsiodras/asn1scc

And a crash-course in using it is here: 

    https://www.thanassis.space/asn1.html

Note also that a new project has just started that will add support for Spark 2014.

Kind regards,
Thanassis Tsiodras, Dr.-Ing.
Real-time Embedded Software Engineer 
System, Software and Technology Department

European Space Agency
ESTEC - Keplerlaan 1, PO Box 299
NL-2200 AG Noordwijk, The Netherlands