Thread: Appetite for Frama-C annotations?

Appetite for Frama-C annotations?

From
Colin Gilbert
Date:
I've been becoming more and more interested in learning formal methods
and wanted to find a good project to which I could contribute. Would
the development team appreciate someone adding ACSL annotations to the
codebase? Are such pull requests likely to be upstreamed? I ask this
because it uses comment syntax to express the specifications and some
people dislike that. However, as we all know, there are solid
advantages to using formal methods, such as automatic test generation
and proven absence of runtime errors.

Looking forward to hearing from you!
Colin



Re: Appetite for Frama-C annotations?

From
Tom Lane
Date:
Colin Gilbert <colingilbert86@gmail.com> writes:
> I've been becoming more and more interested in learning formal methods
> and wanted to find a good project to which I could contribute. Would
> the development team appreciate someone adding ACSL annotations to the
> codebase?

Most likely not.  It might be interesting to see if it's possible to
do anything at all with formal methods in the hairy mess of the Postgres
code base ... but I don't think we'd clutter the code with such comments
unless we thought it'd help the average PG contributor.  Which I doubt.

> Are such pull requests likely to be upstreamed?

We don't do PRs around here --- the project long predates the existence
of git, nevermind github-based workflows, so we're set in other habits.
See

https://wiki.postgresql.org/wiki/Developer_FAQ
https://wiki.postgresql.org/wiki/Submitting_a_Patch

            regards, tom lane



Re: Appetite for Frama-C annotations?

From
Chapman Flack
Date:
On 12/07/21 13:32, Colin Gilbert wrote:
> I've been becoming more and more interested in learning formal methods
> and wanted to find a good project to which I could contribute. Would
> the development team appreciate someone adding ACSL annotations to the
> codebase?

My ears perked up ... I have some Frama-C-related notes-to-self from
a couple years ago that I've not yet pursued, with an interest in how
useful they could be in the hairy mess of the PL/Java extension.

Right at the moment, I am more invested in a somewhat massive
refactoring of the extension. In one sense, tackling the refactoring
without formal tools feels like the wrong order (or working without a net).
It's just that there are only so many hours in the day, and the
refactoring really can't wait, given the backlog of modern capabilities
(like polyglot programming) held back by the current structure. And the
code base should be less hairy afterward, and maybe more amenable to
spec annotations.

According to OpenHub, PL/Java's implementation is currently 74% Java,
19% C. A goal of the current refactoring is to skew that ratio more
heavily Java, with as little C glue remaining as can be achieved.
Meaning, ultimately, a C-specific framework like Frama-C isn't where
most of the fun would be in PL/Java. Still, I'd be interested to see it
in action.

Regards,
-Chap



Re: Appetite for Frama-C annotations?

From
Colin Gilbert
Date:
Hi! Thanks for the quick reply. Are you doing any of this work in a
public repository? If so, could we have a link? There is a similar
idea in Java Modelling Language.  It also uses its own annotations to
describe additional requirements. Are you considering to use it? Maybe
I could help...

On Wed, 8 Dec 2021 at 16:02, Chapman Flack <chap@anastigmatix.net> wrote:
>
> On 12/07/21 13:32, Colin Gilbert wrote:
> > I've been becoming more and more interested in learning formal methods
> > and wanted to find a good project to which I could contribute. Would
> > the development team appreciate someone adding ACSL annotations to the
> > codebase?
>
> My ears perked up ... I have some Frama-C-related notes-to-self from
> a couple years ago that I've not yet pursued, with an interest in how
> useful they could be in the hairy mess of the PL/Java extension.
>
> Right at the moment, I am more invested in a somewhat massive
> refactoring of the extension. In one sense, tackling the refactoring
> without formal tools feels like the wrong order (or working without a net).
> It's just that there are only so many hours in the day, and the
> refactoring really can't wait, given the backlog of modern capabilities
> (like polyglot programming) held back by the current structure. And the
> code base should be less hairy afterward, and maybe more amenable to
> spec annotations.
>
> According to OpenHub, PL/Java's implementation is currently 74% Java,
> 19% C. A goal of the current refactoring is to skew that ratio more
> heavily Java, with as little C glue remaining as can be achieved.
> Meaning, ultimately, a C-specific framework like Frama-C isn't where
> most of the fun would be in PL/Java. Still, I'd be interested to see it
> in action.
>
> Regards,
> -Chap



Re: Appetite for Frama-C annotations?

From
Colin Gilbert
Date:
Thank you very much Tom for your quick reply! If nobody objects to it
too much, I'd focus my work on ensuring full-text-search is
memory-safe.

On Wed, 8 Dec 2021 at 15:21, Tom Lane <tgl@sss.pgh.pa.us> wrote:
>
> Colin Gilbert <colingilbert86@gmail.com> writes:
> > I've been becoming more and more interested in learning formal methods
> > and wanted to find a good project to which I could contribute. Would
> > the development team appreciate someone adding ACSL annotations to the
> > codebase?
>
> Most likely not.  It might be interesting to see if it's possible to
> do anything at all with formal methods in the hairy mess of the Postgres
> code base ... but I don't think we'd clutter the code with such comments
> unless we thought it'd help the average PG contributor.  Which I doubt.
>
> > Are such pull requests likely to be upstreamed?
>
> We don't do PRs around here --- the project long predates the existence
> of git, nevermind github-based workflows, so we're set in other habits.
> See
>
> https://wiki.postgresql.org/wiki/Developer_FAQ
> https://wiki.postgresql.org/wiki/Submitting_a_Patch
>
>                         regards, tom lane



Re: Appetite for Frama-C annotations?

From
Chapman Flack
Date:
On 12/08/21 12:13, Colin Gilbert wrote:
> Hi! Thanks for the quick reply. Are you doing any of this work in a
> public repository? If so, could we have a link? There is a similar
> idea in Java Modelling Language.  It also uses its own annotations to
> describe additional requirements. Are you considering to use it? Maybe
> I could help...

PL/Java's public repository is https://github.com/tada/pljava

Much of the current refactoring I spoke of is not pushed there yet
(it is still in the getting-rebased-a-lot stages). There may be
an initial push of it appearing there in the coming weeks though.

JML is also mentioned in my notes from a couple years back when I was
browsing such tools.

There is also a PL/Java-specific mailing list at
https://www.postgresql.org/list/pljava-dev/

The traffic there is not high.

Regards,
-Chap



Re: Appetite for Frama-C annotations?

From
Laurent Laborde
Date:
Hi there, 

I played a lot with frama-c a long time ago.
Frama-c annotations are very verbose and the result is highly dependent on the skills of the annotator.

Keeping it up-to-date on such a large project with high-speed development will be, in my very humble opinion, extremely difficult.
Perhaps on a sub-project like libpq ?


-- 
Laurent "ker2x" Laborde

On Wed, Dec 8, 2021 at 3:45 PM Colin Gilbert <colingilbert86@gmail.com> wrote:
I've been becoming more and more interested in learning formal methods
and wanted to find a good project to which I could contribute. Would
the development team appreciate someone adding ACSL annotations to the
codebase? Are such pull requests likely to be upstreamed? I ask this
because it uses comment syntax to express the specifications and some
people dislike that. However, as we all know, there are solid
advantages to using formal methods, such as automatic test generation
and proven absence of runtime errors.

Looking forward to hearing from you!
Colin




Re: Appetite for Frama-C annotations?

From
Colin Gilbert
Date:
This is a longer-term plan and I'm going to practice a lot on my own
projects prior. I'm just sending out feelers. My main idea was to
annotate parts of the code that have already been well-established and
validate it while trying to uncover potential edge-cases. I'll do that
at home until something real comes up. If I find a CVE, I know the
address to send that to. An existing project involves other people and
I cannot expect a free hand to dramatically modify the code everyone
else works upon, especially without having proven my worth! I'm
actually really glad for Laurent's suggestion of checking out libpq; I
assume it sees the least rework? That might actually be a fine first
target for some bug-hunting.

As an aside, my desire to validate the FTS is due to its relatively
exposed nature. This is worrying compared to attacks requiring the
ability to craft special tables, prepared statements, or other things
only a developer or admin could do. Would a memory-safe text search
using the existing data structure be best implemented as a plugin?
I've seen adverts for FPGA IP that can access the Postgres data
structures directly from memory so that gives me confidence. Chapman
mentioned polyglot programming; would Postgres ever consider
deprecating unsafe features and replacing them with plugins written in
something like Rust or Ada/SPARK? I write this, hoping not to tread on
a landmine.

I appreciate everyone's engagement!


Colin

On Thu, 9 Dec 2021 at 14:00, Laurent Laborde <kerdezixe@gmail.com> wrote:
>
> Hi there,
>
> I played a lot with frama-c a long time ago.
> Frama-c annotations are very verbose and the result is highly dependent on the skills of the annotator.
>
> Keeping it up-to-date on such a large project with high-speed development will be, in my very humble opinion,
extremelydifficult.
 
> Perhaps on a sub-project like libpq ?
>
>
> --
> Laurent "ker2x" Laborde
>
> On Wed, Dec 8, 2021 at 3:45 PM Colin Gilbert <colingilbert86@gmail.com> wrote:
>>
>> I've been becoming more and more interested in learning formal methods
>> and wanted to find a good project to which I could contribute. Would
>> the development team appreciate someone adding ACSL annotations to the
>> codebase? Are such pull requests likely to be upstreamed? I ask this
>> because it uses comment syntax to express the specifications and some
>> people dislike that. However, as we all know, there are solid
>> advantages to using formal methods, such as automatic test generation
>> and proven absence of runtime errors.
>>
>> Looking forward to hearing from you!
>> Colin
>>
>>
>
>



Re: Appetite for Frama-C annotations?

From
Chapman Flack
Date:
On 12/09/21 12:53, Colin Gilbert wrote:
> ... plugins written in
> something like Rust or Ada/SPARK? I write this, hoping not to tread on

Some work toward supporting "deep" PostgreSQL extensions in Rust
was presented at PGCon 2019 [0].

Regards,
-Chap


[0] https://www.pgcon.org/2019/schedule/events/1322.en.html



Re: Appetite for Frama-C annotations?

From
Dagfinn Ilmari Mannsåker
Date:
Chapman Flack <chap@anastigmatix.net> writes:

> On 12/09/21 12:53, Colin Gilbert wrote:
>> ... plugins written in
>> something like Rust or Ada/SPARK? I write this, hoping not to tread on
>
> Some work toward supporting "deep" PostgreSQL extensions in Rust
> was presented at PGCon 2019 [0].

There's also https://github.com/zombodb/pgx/, which seems more complete
from a quick glance.

https://depth-first.com/articles/2021/08/25/postgres-extensions-in-rust/


- ilmari



Re: Appetite for Frama-C annotations?

From
Colin Gilbert
Date:
Thank you all very much for your inputs! To summarise: I asked about
the possibility of adding ACSL annotations to the codebase and the
responses ranged from nonplussed on one end of the spectrum to some
degree of enthusiasm on the other. It was suggested that libpsql would
be a better initial target than the internals. I appreciated the good,
brisk discussion and if anyone else has any other ideas please let us
all know.

Regards,
Colin