ANN: Ada/SPARK ASN.1 implementation version 0.0.01

ANN: Ada/SPARK ASN.1 implementation version 0.0.01

[Shark8]

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.

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

[Shark8]

It helps if I include the link:

https://github.com/OneWingedShark/ASN.1/

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

[Dmitry A. Kazakov]

On 2016-08-01 10:15, 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 interested in the TLS interface outline. Specifically, in how easy 
it would be to integrate into a non-blocking socket-I/O driven architecture.

That means the TLS layer should write no more data than the output 
buffer length, while keeping its internal state to continue when the 
buffer becomes available, and the layer is called again.

Same when reading data from the input buffer, data get available in 
chunks of arbitrary size. If the layer expects more data, it must return 
to the caller, again, keeping internal state.

This certainly would have impact on the implementation.

P.S. Simple Components presently use GNUTLS for HTTPS, SMTP, MQTT. It 
would be great to have a native Ada TLS instead.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

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

[Shark8]

On Monday, August 1, 2016 at 2:51:56 AM UTC-6, Dmitry A. Kazakov wrote:
> I am interested in the TLS interface outline. Specifically, in how easy 
> it would be to integrate into a non-blocking socket-I/O driven architecture.

There's no outline for the TLS interface, yet. (Even though I did start a TLS project right after Heartbleed, I got stumped on a few points in the RFC [one of which was the ASN.1 OID in certificates] and pretty much abandoned it.)
 
> That means the TLS layer should write no more data than the output 
> buffer length, while keeping its internal state to continue when the 
> buffer becomes available, and the layer is called again.
> 
> Same when reading data from the input buffer, data get available in 
> chunks of arbitrary size. If the layer expects more data, it must return 
> to the caller, again, keeping internal state.

That's a good idea -- a task-type would probably fit the bill nicely, keeping its own state for every instance.

 
> This certainly would have impact on the implementation.

Very much so, but at this point I think outlining the interface would be a bit premature -- at the very least we need the interface for the security certificates, and for that we need an OID type.

> P.S. Simple Components presently use GNUTLS for HTTPS, SMTP, MQTT. It 
> would be great to have a native Ada TLS instead.

*nod* -- I've thought this for literally years, perhaps enough of the community feels the same way as us to actually help implementing it. (And it'll certainly be a good thing if we can make it as SPARK-verifiable as possible.)

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

[Dmitry A. Kazakov]

On 2016-08-01 18:18, Shark8 wrote:
> On Monday, August 1, 2016 at 2:51:56 AM UTC-6, Dmitry A. Kazakov wrote:
>> That means the TLS layer should write no more data than the output
>> buffer length, while keeping its internal state to continue when the
>> buffer becomes available, and the layer is called again.
>>
>> Same when reading data from the input buffer, data get available in
>> chunks of arbitrary size. If the layer expects more data, it must return
>> to the caller, again, keeping internal state.
>
> That's a good idea -- a task-type would probably fit the bill
> nicely,  keeping its own state for every instance.

No task types, please. That would defeat the purpose of the 
architecture. A non-blocking I/O allows multiple connections serviced by 
single task. A connection can also migrate from task to task, e.g. from 
a pool of working tasks.

The method is roughly [for single task scenario]:

loop
    wait for sockets from a set of sockets

    for Socket in sockets ready to read loop
       get connection object from Socket
       read Socket into input FIFO as much as possible w/o blocking
       pass FIFO (unprocessed chuck) to connection object
    end loop;

    for Socket in sockets ready to write loop
       get connection object from Socket
       if not output FIFO full then
          pass FIFO (free chuck) to connection object
       end if;
       write output FIFO as much as possible w/o blocking
    end loop;

end loop;

TLS layer would be a part of connection object. The decoded chunks would 
feed the higher layer. Its output would go back to TLS to encode.

As you see it is more complicated than blocking I/O. Though in the case 
of TLS it could not be very difficult because all packets have fixed 
length. So you possibly could keep internal input and output buffers in 
the TLS layer object.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

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

[Jeffrey R. Carter]

On 08/01/2016 01:15 AM, Shark8 wrote:
> 
> I would certainly appropriate comments, criticism, and most especially contributions.

I took a look at the big-number pkg, and have the following suggestions:

If you want people to contribute to this effort, I'd suggest you use a coding
style more similar to that used in the ARM. You might also want to learn how to
spell "negative".

I don't see why it's desirable to specify the representation of the non-variable
parts of Big_Number.

I'd think it would be a good idea for code like this to be portable, in which
case it should avoid optional types such as Long_Long_Integer, and certainly not
assume it knows that it's 64 bits.

While it's unlikely to be an issue on modern processors, given your constant

Base : constant := 2 ** System.Word_Size;

there's no guarantee that declarations

type Digit is range 0 .. Base;

type Double_Digit is mod Base ** 2;

will be accepted. A more portable approach, and one which maximizes the size of
the digits used, is

type Double_Digit is mod System.Max_Binary_Modulus;

Digit_Size : constant := Double_Digit'Size / 2;

type Digit is mod Digit_Size;

This is the approach used by PragmARC.Unbounded_Integers.

HTH.

-- 
Jeff Carter
"We burst our pimples at you."
Monty Python & the Holy Grail
16

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

[Shark8]

On Monday, August 1, 2016 at 1:47:39 PM UTC-6, Jeffrey R. Carter wrote:
> On 08/01/2016 01:15 AM, Shark8 wrote:
> > 
> > I would certainly appropriate comments, criticism, and most especially contributions.
> 
> I took a look at the big-number pkg, and have the following suggestions:
> 
> If you want people to contribute to this effort, I'd suggest you use a coding
> style more similar to that used in the ARM. You might also want to learn how to
> spell "negative".

Corrected spelling.
Also, "coding style" should **NOT** be an issue -- it is a testament to the CS industry being stunted that it is an issue. (The 'primary' store of source should be within meaningful structures, likely in a DB, not plain=text.)

> I don't see why it's desirable to specify the representation of the non-variable
> parts of Big_Number.
> 
> I'd think it would be a good idea for code like this to be portable, in which
> case it should avoid optional types such as Long_Long_Integer, and certainly not
> assume it knows that it's 64 bits.

Agreed -- however this *is* the 0.0.01 release, and not intended to be the be-all/end-all of source code. (Again, collaboration is welcome.)

> While it's unlikely to be an issue on modern processors, given your constant
> 
> Base : constant := 2 ** System.Word_Size;
> 
> there's no guarantee that declarations
> 
> type Digit is range 0 .. Base;
> 
> type Double_Digit is mod Base ** 2;
> 
> will be accepted. A more portable approach, and one which maximizes the size of
> the digits used, is
> 
> type Double_Digit is mod System.Max_Binary_Modulus;
> 
> Digit_Size : constant := Double_Digit'Size / 2;
> 
> type Digit is mod Digit_Size;
> 
> This is the approach used by PragmARC.Unbounded_Integers.
> 
> HTH.


Thank you for the pointers.

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

[Randy Brukardt]

"Shark8" <onewingedshark@gmail.com> wrote in message 
news:cd2d5a71-69f3-4521-b43d-845dcce053f1@googlegroups.com...
...
> Thank you for the pointers.

That's the best thing to do with pointers/access values: give them to 
someone else. :-) [Or better yet, don't use access types in the first 
place.]

                                            Randy.

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

[Shark8]

On Monday, August 1, 2016 at 4:14:47 PM UTC-6, Randy Brukardt wrote:
>
> That's the best thing to do with pointers/access values: give them to 
> someone else. :-) [Or better yet, don't use access types in the first 
> place.]
> 
>                                             Randy.

LOL -- Exactly my opinion: avoid pointers/accesses where at all possible.
(I'm half tempted to submitto Ada-comment a request to remove anonomous access types from parameter-passing -- it's highly unlikely the ARG would embrace such a code-breaking change... but, on the other hand, it would simplify a lot of things for users/implementors).

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

[Jeffrey R. Carter]

On 08/01/2016 02:55 PM, Shark8 wrote:
> 
> Also, "coding style" should **NOT** be an issue -- it is a testament to the
> CS industry being stunted that it is an issue. (The 'primary' store of source
> should be within meaningful structures, likely in a DB, not plain=text.)

Perhaps. Here in the real world, your source is in plain-text form, and coding
style is an issue.

-- 
Jeff Carter
"Hello! Smelly English K...niggets."
Monty Python & the Holy Grail
08

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

[Shark8]

On Monday, August 1, 2016 at 5:42:45 PM UTC-6, Jeffrey R. Carter wrote:
> 
> Perhaps. Here in the real world, your source is in plain-text form, and coding
> style is an issue.

That is something I'm actually trying to resolve -- I'm seriously considering having Byron have a [improved] DIANA layer optimized for DB storage which would be the basis for a "package manager" (thus allowing an architecture which would render continuous-integration obsolete and ensure consistency across libraries/dependencies).

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

[Jeffrey R. Carter]

On 08/01/2016 04:53 PM, Shark8 wrote:
> 
> That is something I'm actually trying to resolve -- I'm seriously considering
> having Byron have a [improved] DIANA layer optimized for DB storage which
> would be the basis for a "package manager" (thus allowing an architecture
> which would render continuous-integration obsolete and ensure consistency
> across libraries/dependencies).

The Rational tools store programs as DIANA, and the text version you see is
generated from that, and any changes are parsed and redisplayed on the fly.
Obviously, it didn't catch on.

-- 
Jeff Carter
"Hello! Smelly English K...niggets."
Monty Python & the Holy Grail
08

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

[ttsiodras]

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

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

[p.p11]

Hello,

By when do you plan to upgrade to SPARK 2014?

Thanks, Pascal.

Le mardi 2 août 2016 11:01:19 UTC+2, ttsi...@gmail.com a écrit :
> 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

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

[ttsiodras]

The project contract has just been signed, and will kickoff after the summer vacations. The expected duration of the work is 12 months, with development done in the open (in a branch on the GitHub repo). 

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,
> 
> By when do you plan to upgrade to SPARK 2014?
> 
> Thanks, Pascal.
> 
> Le mardi 2 août 2016 11:01:19 UTC+2, ttsi...@gmail.com a écrit :
> > 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