4 ms·

Abstract interpreters and static analyzers are really powerful and not that hard to implement, compared to the little competition we have in this space. I am s

by nextos 4y ago

Abstract interpreters and static analyzers are really powerful and not that hard to implement, compared to the little competition we have in this space. I am surprised with the lack of startups in the area. It's just a bit of abstract algebra. With Datalog, the barrier of entry is pretty low: https://arxiv.org/abs/2012.10086 https://arxiv.org/abs/2012.10086 I have personally implemented a few of the features provided by Astrée, e.g. array bounds check, using the ideas described in: https://link.springer.com/book/10.1007/978-3-662-03811-6 https://link.springer.com/book/10.1007/978-3-662-03811-6

edwcross 4y ago
There are probably others, but this is one such startup: https://trust-in-soft.com/ https://trust-in-soft.com/
aseipp 4y ago
It's difficult to fund enough skilled programmers to work on stuff like this full time, and productionize the results in a coherent product. A good example is a sibling comment that says "it would mostly be easy except for the GUI" and that's assuming "no allocations." The things customers pay you for are often the hard parts like that stuff, not the theoretical parts you can enjoy from a PDF. It sucks, but it's true: you're selling a production quality tool to picky-ass programmers. I say this as someone who has a copy of that book you mentioned and has implemented type systems, domain specific analyzers, used datalog (Souffle) a lot, etc. You also need to know your competition, and the story is even worse there. As I've watched security engineering advance over the years -- and I know you aren't specifically talking about security, but go with me here -- one of the only methods that has actually gone from "nascent infosec curiosity" into full-blown large scale usage by major and minor players has been fuzzing, which most people know as just "throw random shit at it until it breaks". That's because it's often easy to integrate, has few visible thorns in practice, has a surprisingly high signal-to-noise ratio, and can be performed even with duct tape and glue on an existing codebase. It can be done in any language. It often delivers positive results immediately in the short term and continuously over time. That's actually what your userbase considers "easy to implement", not "learn datalog and abstract algebra to understand and integrate domain specific static analyzers into your build system." Is it powerful? Yes, and I like solutions like CodeQL or MIRAI (for Rust). Do they have long term benefits? I think so. Is it easy or at least "not that hard"? I'm not immediately convinced.
HybridCurve 4y ago
It is not that difficult to implement -some- basic features of static analysis or abstract interpretation. The problem complexity in this area is enormous and it quickly becomes difficult to manage aspects of path exploration and satisfiability effectively. This is why fuzzing has been more popular method since it is not as difficult to implement and produces reasonable results.
intelVISA 4y ago
Outside of regulated fields like healthcare and travel is the market even significant for such tooling? Can't say I know any shop that prioritizes code correctness outside of press releases.
- GuB-42 4y ago
  You can add energy and defense to the list. And regulated fields are a big market, not just the huge companies that work in this field (you can see a short list on the linked page), but also suppliers of these companies.
- defrost 4y ago
  Geophysical data aquisition, processing, interpretation. Fire simulation modelling. Computational GIS tooling (Hexagon et al) Computational Algebra (eg Cayley|Magma) Fireball monitoring, Square Kilometre Array processing, . . . I'm struggling to recall anything I've worked on that didn't emphasis code correctness.
- jamesfinlayson 4y ago
  If there's a high enough risk, maybe. I've worked in gambling (regulated, but not to the same degree as something that's life and death) and the security team has pushed for the use of tools like this.
- ryao 4y ago
  I am interested in using it on OpenZFS. I will probably try the trial in a couple months. Assuming that it does well, it is unfortunate that I will not be able to use it beyond the trial period, since I expect the price to be too expensive.
  - nextos 4y ago
    That's my point, IMHO this is much more useful than LLM-autocompletion right now. But there are so few options available, at such a high cost, that nobody uses them. Abstract interpretation / static analysis can detect lots of defects automatically.
ryao 4y ago
I thought abstraction interpretation on the level that astree claims to implement is supposed to be extremely hard, which is why almost nobody else tries to do it. I only know of two that try: http://kestreltechnology.com/technology.html http://kestreltechnology.com/technology.html https://github.com/NASA-SW-VnV/ikos https://github.com/NASA-SW-VnV/ikos
- edwcross 4y ago
  Also Frama-C/Eva: https://www.frama-c.com/fc-plugins/eva.html https://www.frama-c.com/fc-plugins/eva.html
  - mdaniel 4y ago
    It took some eagle eye to spot the link, but they have the source in a self-hosted copy of gitlab: https://git.frama-c.com/pub/frama-c https://git.frama-c.com/pub/frama-c and a sibling repo is also interesting where they seem to apply analysis to some open source code as an example: https://git.frama-c.com/pub/open-source-case-studies https://git.frama-c.com/pub/open-source-case-studies
- mschnell 4y ago
  You can add grammatech‘s codesonar
  - marmetio 4y ago
    I believe the "level" referred to is soundness. Codesonar is self-admittedly not sound [1], and instead focuses on other valuable aspects of static analysis. It's a different type of tool. [1] https://blogs.grammatech.com/how-sound-static-analysis-complements-heuristic-analysis https://blogs.grammatech.com/how-sound-static-analysis-compl...
- quentinkent1 4y ago
  Also Mathworks Polyspace Code Prover: https://mathworks.com/products/polyspace-code-prover.html https://mathworks.com/products/polyspace-code-prover.html

by nextos 4y ago

edwcross 4y ago

There are probably others, but this is one such startup: https://trust-in-soft.com/ https://trust-in-soft.com/

aseipp 4y ago

It's difficult to fund enough skilled programmers to work on stuff like this full time, and productionize the results in a coherent product. A good example is a sibling comment that says "it would mostly be easy except for the GUI" and that's assuming "no allocations." The things customers pay you for are often the hard parts like that stuff, not the theoretical parts you can enjoy from a PDF. It sucks, but it's true: you're selling a production quality tool to picky-ass programmers. I say this as someone who has a copy of that book you mentioned and has implemented type systems, domain specific analyzers, used datalog (Souffle) a lot, etc. You also need to know your competition, and the story is even worse there. As I've watched security engineering advance over the years -- and I know you aren't specifically talking about security, but go with me here -- one of the only methods that has actually gone from "nascent infosec curiosity" into full-blown large scale usage by major and minor players has been fuzzing, which most people know as just "throw random shit at it until it breaks". That's because it's often easy to integrate, has few visible thorns in practice, has a surprisingly high signal-to-noise ratio, and can be performed even with duct tape and glue on an existing codebase. It can be done in any language. It often delivers positive results immediately in the short term and continuously over time. That's actually what your userbase considers "easy to implement", not "learn datalog and abstract algebra to understand and integrate domain specific static analyzers into your build system." Is it powerful? Yes, and I like solutions like CodeQL or MIRAI (for Rust). Do they have long term benefits? I think so. Is it easy or at least "not that hard"? I'm not immediately convinced.

HybridCurve 4y ago

It is not that difficult to implement -some- basic features of static analysis or abstract interpretation. The problem complexity in this area is enormous and it quickly becomes difficult to manage aspects of path exploration and satisfiability effectively. This is why fuzzing has been more popular method since it is not as difficult to implement and produces reasonable results.

intelVISA 4y ago

Outside of regulated fields like healthcare and travel is the market even significant for such tooling? Can't say I know any shop that prioritizes code correctness outside of press releases.

GuB-42 4y ago
You can add energy and defense to the list. And regulated fields are a big market, not just the huge companies that work in this field (you can see a short list on the linked page), but also suppliers of these companies.
defrost 4y ago
Geophysical data aquisition, processing, interpretation. Fire simulation modelling. Computational GIS tooling (Hexagon et al) Computational Algebra (eg Cayley|Magma) Fireball monitoring, Square Kilometre Array processing, . . . I'm struggling to recall anything I've worked on that didn't emphasis code correctness.
jamesfinlayson 4y ago
If there's a high enough risk, maybe. I've worked in gambling (regulated, but not to the same degree as something that's life and death) and the security team has pushed for the use of tools like this.
ryao 4y ago
I am interested in using it on OpenZFS. I will probably try the trial in a couple months. Assuming that it does well, it is unfortunate that I will not be able to use it beyond the trial period, since I expect the price to be too expensive.
- nextos 4y ago
  That's my point, IMHO this is much more useful than LLM-autocompletion right now. But there are so few options available, at such a high cost, that nobody uses them. Abstract interpretation / static analysis can detect lots of defects automatically.

ryao 4y ago

I thought abstraction interpretation on the level that astree claims to implement is supposed to be extremely hard, which is why almost nobody else tries to do it. I only know of two that try: http://kestreltechnology.com/technology.html http://kestreltechnology.com/technology.html https://github.com/NASA-SW-VnV/ikos https://github.com/NASA-SW-VnV/ikos

edwcross 4y ago
Also Frama-C/Eva: https://www.frama-c.com/fc-plugins/eva.html https://www.frama-c.com/fc-plugins/eva.html
- mdaniel 4y ago
  It took some eagle eye to spot the link, but they have the source in a self-hosted copy of gitlab: https://git.frama-c.com/pub/frama-c https://git.frama-c.com/pub/frama-c and a sibling repo is also interesting where they seem to apply analysis to some open source code as an example: https://git.frama-c.com/pub/open-source-case-studies https://git.frama-c.com/pub/open-source-case-studies
mschnell 4y ago
You can add grammatech‘s codesonar
- marmetio 4y ago
  I believe the "level" referred to is soundness. Codesonar is self-admittedly not sound [1], and instead focuses on other valuable aspects of static analysis. It's a different type of tool. [1] https://blogs.grammatech.com/how-sound-static-analysis-complements-heuristic-analysis https://blogs.grammatech.com/how-sound-static-analysis-compl...
quentinkent1 4y ago
Also Mathworks Polyspace Code Prover: https://mathworks.com/products/polyspace-code-prover.html https://mathworks.com/products/polyspace-code-prover.html