3 ms·

This is a really cool paper with impressive results. An interesting property that this paper doesn't consider (I believe the language described does not allow

by awirth 9y ago

This is a really cool paper with impressive results. An interesting property that this paper doesn't consider (I believe the language described does not allow it though) is casting pointers/references to integers. Many languages consider this unsafe, but Rust does not. Considering casting pointers to integers unsafe prevents 'address disclosure' vulnerabilities, which is relevant in the context of any program that incorporates (potentially buggy) unsafe code (read: all of them). This can be used to defeat ASLR.

Lucretia9000 9y ago
Ada.Unchecked_Conversion?
- touisteur 9y ago
  More like the safer : http://www.adaic.org/resources/add_content/standards/05rm/html/RM-13-7-2.html http://www.adaic.org/resources/add_content/standards/05rm/ht... ? And to display addresses (with GNAT only...) : https://www2.adacore.com/gap-static/GNAT_Book/html/rts/s-addima__ads.htm https://www2.adacore.com/gap-static/GNAT_Book/html/rts/s-add... . Nothing preventing you to display addresses anyway. Surely something I've reached only once or twice in 10+ years of Ada. I'm left wondering how one could debug low-level stuff without it. Sure you can use gdb, valgrind. But sometimes you can't. You can probably make this a coding rule and find something to check it in Gnatcheck (http://docs.adacore.com/live/wave/asis/html/gnatcheck_rm/gnatcheck_rm/predefined_rules.html#unchecked-address-conversions http://docs.adacore.com/live/wave/asis/html/gnatcheck_rm/gna...) or AdaControl (http://www.adalog.fr/en/AdaControl.html http://www.adalog.fr/en/AdaControl.html). Something you can do with ASIS (https://en.m.wikipedia.org/wiki/Ada_Semantic_Interface_Specification https://en.m.wikipedia.org/wiki/Ada_Semantic_Interface_Speci...) or libadalang (http://blog.adacore.com/introducing-libadalang http://blog.adacore.com/introducing-libadalang) is to build your own linter to check the use of this kind of operations. For the curious about pointers in Ada (it is sometimes a bit confusing if you're coming from the pointer-is-an-integer-like-an-other-right? crowd, as I once was) : https://en.m.wikibooks.org/wiki/Ada_Programming/Types/access https://en.m.wikibooks.org/wiki/Ada_Programming/Types/access. It barely scrapes the surface but for a nicer introduction I can only recommend the 'Barnes' (http://www.cambridge.org/fr/academic/subjects/computer-science/software-engineering-and-development/programming-ada-2012?format=PB&isbn=9781107424814 http://www.cambridge.org/fr/academic/subjects/computer-scien...) in dead-tree form or a gentle introduction by JP Rosen at FOSDEM 2016 (pdf) : https://people.cs.kuleuven.be/~dirk.craeynest/ada-belgium/events/16/160130-fosdem/09-ada-memory.pdf https://people.cs.kuleuven.be/~dirk.craeynest/ada-belgium/ev...
kibwen 9y ago
The `unsafe` keyword in Rust isn't about preventing general security vulnerabilities though, it's about denoting parts of the code where proof of memory safety has to be determined by hand.

by awirth 9y ago

Lucretia9000 9y ago

Ada.Unchecked_Conversion?

touisteur 9y ago
More like the safer : http://www.adaic.org/resources/add_content/standards/05rm/html/RM-13-7-2.html http://www.adaic.org/resources/add_content/standards/05rm/ht... ? And to display addresses (with GNAT only...) : https://www2.adacore.com/gap-static/GNAT_Book/html/rts/s-addima__ads.htm https://www2.adacore.com/gap-static/GNAT_Book/html/rts/s-add... . Nothing preventing you to display addresses anyway. Surely something I've reached only once or twice in 10+ years of Ada. I'm left wondering how one could debug low-level stuff without it. Sure you can use gdb, valgrind. But sometimes you can't. You can probably make this a coding rule and find something to check it in Gnatcheck (http://docs.adacore.com/live/wave/asis/html/gnatcheck_rm/gnatcheck_rm/predefined_rules.html#unchecked-address-conversions http://docs.adacore.com/live/wave/asis/html/gnatcheck_rm/gna...) or AdaControl (http://www.adalog.fr/en/AdaControl.html http://www.adalog.fr/en/AdaControl.html). Something you can do with ASIS (https://en.m.wikipedia.org/wiki/Ada_Semantic_Interface_Specification https://en.m.wikipedia.org/wiki/Ada_Semantic_Interface_Speci...) or libadalang (http://blog.adacore.com/introducing-libadalang http://blog.adacore.com/introducing-libadalang) is to build your own linter to check the use of this kind of operations. For the curious about pointers in Ada (it is sometimes a bit confusing if you're coming from the pointer-is-an-integer-like-an-other-right? crowd, as I once was) : https://en.m.wikibooks.org/wiki/Ada_Programming/Types/access https://en.m.wikibooks.org/wiki/Ada_Programming/Types/access. It barely scrapes the surface but for a nicer introduction I can only recommend the 'Barnes' (http://www.cambridge.org/fr/academic/subjects/computer-science/software-engineering-and-development/programming-ada-2012?format=PB&isbn=9781107424814 http://www.cambridge.org/fr/academic/subjects/computer-scien...) in dead-tree form or a gentle introduction by JP Rosen at FOSDEM 2016 (pdf) : https://people.cs.kuleuven.be/~dirk.craeynest/ada-belgium/events/16/160130-fosdem/09-ada-memory.pdf https://people.cs.kuleuven.be/~dirk.craeynest/ada-belgium/ev...

kibwen 9y ago

The `unsafe` keyword in Rust isn't about preventing general security vulnerabilities though, it's about denoting parts of the code where proof of memory safety has to be determined by hand.