From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=0.1 required=5.0 tests=BAYES_00,FREEMAIL_FROM, PDS_OTHER_BAD_TLD autolearn=no autolearn_force=no version=3.4.4 X-Received: by 10.176.3.214 with SMTP id 80mr56702321uau.4.1470208436980; Wed, 03 Aug 2016 00:13:56 -0700 (PDT) X-Received: by 10.157.40.148 with SMTP id s20mr3919755ota.6.1470208436907; Wed, 03 Aug 2016 00:13:56 -0700 (PDT) Path: eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!news.eternal-september.org!feeder.eternal-september.org!news.glorb.com!j37no6398173qta.0!news-out.google.com!d68ni15392ith.0!nntp.google.com!f6no6942776ith.0!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail Newsgroups: comp.lang.ada Date: Wed, 3 Aug 2016 00:13:56 -0700 (PDT) In-Reply-To: <5a686bf2-3af8-489b-b66b-dccbbaa4cdcb@googlegroups.com> Complaints-To: groups-abuse@google.com Injection-Info: glegroupsg2000goo.googlegroups.com; posting-host=131.176.243.10; posting-account=vAdwtwoAAADu7BhtlMbtGYCmhpGTXjuP NNTP-Posting-Host: 131.176.243.10 References: <3ac0fbcd-1f1c-40b8-b030-de03954f894f@googlegroups.com> <5a686bf2-3af8-489b-b66b-dccbbaa4cdcb@googlegroups.com> User-Agent: G2/1.0 MIME-Version: 1.0 Message-ID: Subject: Re: ANN: Ada/SPARK ASN.1 implementation version 0.0.01 From: ttsiodras@gmail.com Injection-Date: Wed, 03 Aug 2016 07:13:56 +0000 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable Xref: news.eternal-september.org comp.lang.ada:31263 Date: 2016-08-03T00:13:56-07:00 List-Id: The project contract has just been signed, and will kickoff after the summe= r vacations. The expected duration of the work is 12 months, with developme= nt done in the open (in a branch on the GitHub repo).=20 Based on past experiences, we anticipare working versions (i.e. with SPARK = 2014 support) a lot sooner than 12 months. Feel free to chime in with tickets/comments - we welcome your feedback. Kind regards, Thanassis. On Tuesday, August 2, 2016 at 8:47:59 PM UTC+2, p....@orange.fr wrote: > Hello, >=20 > By when do you plan to upgrade to SPARK 2014? >=20 > Thanks, Pascal. >=20 > Le mardi 2 ao=C3=BBt 2016 11:01:19 UTC+2, ttsi...@gmail.com a =C3=A9crit= =C2=A0: > > 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 implem= entation of ASN.1, which is used in security-certificates, which is hopeful= ly the first step in a verified-TLS/-TLS -- the project also aims to be [di= rectly] usable in DSA projects. > > >=20 > > > As of 0.0.01 the only portion implemented is a pure big-number packag= e, and another currently shared-passive unit for usability.=20 > > >=20 > > > I would certainly appropriate comments, criticism, and most especiall= y contributions. > >=20 > > I am not sure if it can be used with the TLS ASN.1 grammar - but I thin= k it's worth checking out our own open-source ASN.1 compiler, targetting bo= th C and Spark/Ada (developed under the auspices of the European Space Agen= cy, so targeting the same kind of safety-critical targets you probably have= in mind). > >=20 > > The compiler is here:=20 > >=20 > > https://github.com/ttsiodras/asn1scc > >=20 > > And a crash-course in using it is here:=20 > >=20 > > https://www.thanassis.space/asn1.html > >=20 > > Note also that a new project has just started that will add support for= Spark 2014. > >=20 > > Kind regards, > > Thanassis Tsiodras, Dr.-Ing. > > Real-time Embedded Software Engineer=20 > > System, Software and Technology Department > >=20 > > European Space Agency > > ESTEC - Keplerlaan 1, PO Box 299 > > NL-2200 AG Noordwijk, The Netherlands