13 ms·

Nagini: A Static Verifier for Python [pdf]

102 points by Klasiaster 8y ago

Klasiaster 8y ago
Abstract copied from the PDF: We present Nagini, an automated, modular verifier for statically-typed, concurrent Python 3 programs, built on the Viper verification infrastructure. Combining established concepts with new ideas, Nagini can verify memory safety, functional properties, termination, deadlock freedom, and input/output behavior. Our experiments show that Nagini is able to verify non-trivial properties of real-world Python code.
- rcthompson 8y ago
  What exactly does verifying memory safety mean in Python? What memory-unsafe operations does Python allow?
  - UncleEntity 8y ago
    I think (maybe) they mean something like: x = Foo() thread1.do_something_to_foo(x) thread2.do_something_to_foo(x) wait_on_threads(thread1, thread2) # however that works in python? do_something_to_modified_foo(x)
    - rcthompson 8y ago
      Wouldn't that be thread safety? I thought memory safety was things like preventing access to uninitialized or freed memory. As far as I know there's no way to do such things in pure Python.
  - marcoeilers 8y ago
    We use the term "memory safety" very broadly; what we meant was the absence of runtime errors (e.g., out-of-bounds list accesses), uncaught exceptions, concurrent modification, basically anything that would lead the program to crash. Those aren't memory unsafe in the original sense of the word in Python, but they still crash the program. Additionally, we prove the absence of data races between threads.
Animats 8y ago
Classic, and nicely done. They did something right that's rarely done - their verification extensions to Python are Pythonic. They don't use a separate language for invariants and assertions, and they don't put the assertions in comments. The assertions are thus part of the program.
btown 8y ago
This is really, really cool. It's on github at https://github.com/marcoeilers/nagini https://github.com/marcoeilers/nagini and you can see examples of the syntax here: http://viper.ethz.ch/nagini-examples/ http://viper.ethz.ch/nagini-examples/ In the same way that Python's (and Flow/Typescript's) typing lets you describe argument and return types with no more effort/characters than typing a comment, this lets you describe invariants and assertions exactly where you normally would with comments, including invariants on each element of a sequence... and instantly get static typing. I believe there's a custom meta_path importer so it will strip out at module load time, making it zero-cost at runtime. It's the type of thing that there's no reason not to use. It's powered by Viper, and you can see pseudocode of the internal representation it gets transpiled to in Figure 4 here: http://people.inf.ethz.ch/summersa/wiki/lib/exe/fetch.php?media=papers:viper-vmcai16.pdf http://people.inf.ethz.ch/summersa/wiki/lib/exe/fetch.php?me... . Very smart stuff around tracking read/write dependencies on variables in a programmer-friendly way.
- sametmax 8y ago
  I'm not sure I understand the benefit. We already have type hints, and for more complicated tests, assert. Both can be ignored in production. EDIT: ok, I get that they provide some additional benefits such as checking for deadlock or memory leaks. Neat.
  - btown 8y ago
    Assertions, combined with highly granular code coverage (which most [all?] Python coverage libraries can only do at a line level, so this isn't really sufficient), can almost get you to a point where you're confident that all your asserted invariants are true for all inputs. Statically checking/proving that those invariants will hold, regardless of inputs, is a huge step up in that level of confidence.
gigatexal 8y ago
I’m going to get blasted on this but what if all this python static type checking and such is not needed. Python is python. It’s slower than other languages and that’s ok. I fear that too much is being done and slowly the clean syntax of the language is being eroded.
- abakus 8y ago
  THis. I think the type hint system adds so much visual noise it starts to look like perl. When an attempt to build huge (100k+) project with Python failes, it is not because of the duck typing, but simply because Python is not designed for such use cases.
  - stochastic_monk 8y ago
    For me, past ~3000 lines, I really work best in a statically compiled language. The type-checking allows me to catch most bugs at compile-time.
    - hobls 8y ago
      Same. I LOVE Python, but if I want to take a project particularly far I tend to end up porting it to a static language. (Usually go these days.)
      - gigatexal 8y ago
        We almost switched to go at my little startup mostly because of gokit but the syntax is so abhorrent at least to me. I am glad we didn’t. I know it’s peobably stupid to make such a choice but programmer happiness for me comes in part to the syntax and cleanliness of the code. Something I didn’t see in Go
        hobls 8y ago
        What did you end up going with? I like hearing what problems a language is solving well. :)
kjeetgill 8y ago
Fun fact: The name, Nagini, derives from the Sanskrit word for "a deity or class of entity or being taking the form of a very great snake, specifically the king cobra, found in the Indian religions of Hinduism, Buddhism and Jainism." https://en.wikipedia.org/wiki/N%C4%81ga https://en.wikipedia.org/wiki/N%C4%81ga
- adw 8y ago
  Which is no doubt the source for the name Nagini in the Harry Potter books (the familiar of the big bad, Lord Voldemort; a magically-enhanced snake.)
  - marcoeilers 8y ago
    We actually named it after the Harry Potter snake :) There was a wiki at some point that stated that Nagini was a hybrid between a Python and a Viper (Viper is the verification framework that we build on), so that's why.
45455 8y ago
nhvbk [ki['m;,ln
45455 8y ago
kbhkhk b;jmonh
45455 8y ago
yntgbbhyf
marcoeilers 8y ago
Hi everyone, I'm the main author of the tool; it's really cool to see that there's some interest in this :) If you have any questions, I'd be happy to answer them.

102 points by Klasiaster 8y ago

Abstract copied from the PDF: We present Nagini, an automated, modular verifier for statically-typed, concurrent Python 3 programs, built on the Viper verification infrastructure. Combining established concepts with new ideas, Nagini can verify memory safety, functional properties, termination, deadlock freedom, and input/output behavior. Our experiments show that Nagini is able to verify non-trivial properties of real-world Python code.

rcthompson 8y ago
What exactly does verifying memory safety mean in Python? What memory-unsafe operations does Python allow?
- UncleEntity 8y ago
  I think (maybe) they mean something like: x = Foo() thread1.do_something_to_foo(x) thread2.do_something_to_foo(x) wait_on_threads(thread1, thread2) # however that works in python? do_something_to_modified_foo(x)
  - rcthompson 8y ago
    Wouldn't that be thread safety? I thought memory safety was things like preventing access to uninitialized or freed memory. As far as I know there's no way to do such things in pure Python.
- marcoeilers 8y ago
  We use the term "memory safety" very broadly; what we meant was the absence of runtime errors (e.g., out-of-bounds list accesses), uncaught exceptions, concurrent modification, basically anything that would lead the program to crash. Those aren't memory unsafe in the original sense of the word in Python, but they still crash the program. Additionally, we prove the absence of data races between threads.

Animats 8y ago

Classic, and nicely done. They did something right that's rarely done - their verification extensions to Python are Pythonic. They don't use a separate language for invariants and assertions, and they don't put the assertions in comments. The assertions are thus part of the program.

btown 8y ago

This is really, really cool. It's on github at https://github.com/marcoeilers/nagini https://github.com/marcoeilers/nagini and you can see examples of the syntax here: http://viper.ethz.ch/nagini-examples/ http://viper.ethz.ch/nagini-examples/ In the same way that Python's (and Flow/Typescript's) typing lets you describe argument and return types with no more effort/characters than typing a comment, this lets you describe invariants and assertions exactly where you normally would with comments, including invariants on each element of a sequence... and instantly get static typing. I believe there's a custom meta_path importer so it will strip out at module load time, making it zero-cost at runtime. It's the type of thing that there's no reason not to use. It's powered by Viper, and you can see pseudocode of the internal representation it gets transpiled to in Figure 4 here: http://people.inf.ethz.ch/summersa/wiki/lib/exe/fetch.php?media=papers:viper-vmcai16.pdf http://people.inf.ethz.ch/summersa/wiki/lib/exe/fetch.php?me... . Very smart stuff around tracking read/write dependencies on variables in a programmer-friendly way.

sametmax 8y ago
I'm not sure I understand the benefit. We already have type hints, and for more complicated tests, assert. Both can be ignored in production. EDIT: ok, I get that they provide some additional benefits such as checking for deadlock or memory leaks. Neat.
- btown 8y ago
  Assertions, combined with highly granular code coverage (which most [all?] Python coverage libraries can only do at a line level, so this isn't really sufficient), can almost get you to a point where you're confident that all your asserted invariants are true for all inputs. Statically checking/proving that those invariants will hold, regardless of inputs, is a huge step up in that level of confidence.

gigatexal 8y ago

I’m going to get blasted on this but what if all this python static type checking and such is not needed. Python is python. It’s slower than other languages and that’s ok. I fear that too much is being done and slowly the clean syntax of the language is being eroded.

abakus 8y ago
THis. I think the type hint system adds so much visual noise it starts to look like perl. When an attempt to build huge (100k+) project with Python failes, it is not because of the duck typing, but simply because Python is not designed for such use cases.
- stochastic_monk 8y ago
  For me, past ~3000 lines, I really work best in a statically compiled language. The type-checking allows me to catch most bugs at compile-time.
  - hobls 8y ago
    Same. I LOVE Python, but if I want to take a project particularly far I tend to end up porting it to a static language. (Usually go these days.)
    - gigatexal 8y ago
      We almost switched to go at my little startup mostly because of gokit but the syntax is so abhorrent at least to me. I am glad we didn’t. I know it’s peobably stupid to make such a choice but programmer happiness for me comes in part to the syntax and cleanliness of the code. Something I didn’t see in Go
      - hobls 8y ago
        What did you end up going with? I like hearing what problems a language is solving well. :)

kjeetgill 8y ago

Fun fact: The name, Nagini, derives from the Sanskrit word for "a deity or class of entity or being taking the form of a very great snake, specifically the king cobra, found in the Indian religions of Hinduism, Buddhism and Jainism." https://en.wikipedia.org/wiki/N%C4%81ga https://en.wikipedia.org/wiki/N%C4%81ga

adw 8y ago
Which is no doubt the source for the name Nagini in the Harry Potter books (the familiar of the big bad, Lord Voldemort; a magically-enhanced snake.)
- marcoeilers 8y ago
  We actually named it after the Harry Potter snake :) There was a wiki at some point that stated that Nagini was a hybrid between a Python and a Viper (Viper is the verification framework that we build on), so that's why.

45455 8y ago

nhvbk [ki['m;,ln

45455 8y ago

kbhkhk b;jmonh

45455 8y ago

yntgbbhyf

marcoeilers 8y ago

Hi everyone, I'm the main author of the tool; it's really cool to see that there's some interest in this :) If you have any questions, I'd be happy to answer them.