6 ms·

This may be helpful for the DNS server https://github.com/gtadam/rust-dns https://github.com/gtadam/rust-dns

nickpsecurity 11y ago
Interesting. So will this for anyone brave enough to use SPARK and Rust: http://ironsides.martincarlisle.com/ http://ironsides.martincarlisle.com/ IRONSIDES uses SPARK to show freedom of exceptions or single-packet DOS. A translation to Rust would probably preserve most of those properties. I also thought a parallel development between Ada2012/SPARK and Rust would be interesting to see if one set of checkers catch something another misses in same piece of software.
- fghfghgfhfg 11y ago
  My understanding is that Rust doesn't have so much to offer Ada/SPARK. I haven't looked that hard at Rust though, so maybe I've overlooked some of it's features. You have to jump through the same sort of hoops in Rust as you do C++ to get the sort of basic type safety found in Ada/SPARK. Rust doesn't so much have a focus on safety and correctness in general, as a focus on memory safety. Admittedly, Ada/SPARK doesn't make the kinds of guarantees that Rust does about memory. However, accessibility checks help prevent dangling pointers and the use of memory subpools can avoid the need for explicit frees. Additionally, Ada offers some features like the ability to return a dynamically sized array as if it were on the stack which helps reduce how often memory needs to be manually managed. I believe SPARK may not allow this sort of thing though. I'm also not sure why you would want to abandon the actually verified properties of Ironsides for a hope those properties remained in an unverified port.
  - nickpsecurity 11y ago
    "My understanding is that Rust doesn't have so much to offer Ada/SPARK. I haven't looked that hard at Rust though, so maybe I've overlooked some of it's features." I liked the juxtaposition of that haha. It kind of negates anything about Rust in your counterpoint. Your points on Ada/SPARK are still worthwhile. "Ada offers..." No doubt. It was systematically designed to reduce the existence or impact of flaws throughout software. They kept this up in extensions. SPARK straight up proves the absence of them in a subset. So, it's what my gold standard is for safe, systems programming. Rust is the newcomer with interesting additions inspired by safer-than-C imperative and functional languages. It's confusing scheme for memory and concurrency protection is said to be quite effective. It might end up better than Ada over time or just different tradeoffs. The important thing, though, is that it has what Ada/SPARK will likely never have: large-scale adoption with uptake by big companies and users who will add to its ecosystem. Ada FOSS community is barely there with biggest deliverables coming from AdaCore. Remember Gabriel's Worse is Better? Real lesson of it is certain things get adoption better than others. Best to bet on them. Rust is in that category a bit but with Right Thing elements. So, it's worth investing in for long-term benefit of IT. "I'm also not sure why you would want to abandon the actually verified properties of Ironsides for a hope those properties remained in an unverified port." I'm not necessarily suggesting that. There's a reason that OpenBSD and some proprietary vendors keep their system working on several compilers. There's a reason NASA project here used 4 static analysis tools. There's a reason B3/A1 systems kept detailed, formal specs side-by-side with code with both checked. The reason is that different tools catch different types of problems. Further, a problem detected in one might apply to the other. Now, a semantic difference exists between Ada/SPARK and Rust. Yet, there's usually a subset and/or style one can use where results from one about memory or control issues will apply to the other. So, I said do it in parallel: both Ada/SPARK mix and Rust. It displays how each language handles the problem. It let's the analysis tools of each check it for problems that might exist in both. Tool version of many eyeballs except works consistently. ;) It also means that compiler optimization problems in one might not affect an other. Can help with hotfixes while compiler team develops guidance or patches. Also, provides two implementations that can help with adoption and support. There's an issue of maintaining parity but the simpler version is write it in Ada/SPARK w/ Rust release getting uptake. That's the lines I was thinking on. Rust is popular and better than usual. Ada is equal or better in capabilities but not going anywhere. Leverage both to get benefits of both maybe defaulting on Rust release for adoption. Far as Ada vs Rust, I'd like a less biased party that knows Rust's protections and features through and through to do a comparison for me. I have a reference listing each issue Ada tackles and how. I probably can dig up one for SPARK 2014, too. I would love to see what mainstream answer to Ada can do vs the baseline it created. Note: You should get a real account if you're a programmer AND know Ada/SPARK. Seriously under-represented here.
    - fghfghgfhfg 11y ago
      "I liked the juxtaposition of that haha. It kind of negates anything about Rust in your counterpoint." I almost removed that at the end. I wasn't trying to say much about Rust except that it wasn't predicated on this idea of quickly spinning up new, conceptual types with specific constraints like Ada/SPARK. That sort of thing is really either infused throughout a language, or it isn't used. It doesn't take a great deal of familiarity to see that much. Actually, just for this response I went and looked into it a little more. Rust has a tiny bit of syntax sugar for creating structs with positional members. So, you can at least wrap things in a struct a little bit easier than in C++, as you don't need to name the internal value. That's really not enough. Really I mostly wanted to show that Ada also has some means of helping with memory safety - while also being focused on safety/correctness in general. I suppose on that front (and while I'm pushing Ada anyway) I should also mention Ada has a built-in concurrency model, although I suspect you may already be aware of this. "Ada FOSS community is barely there with biggest deliverables coming from AdaCore." Yeah, this is the biggest bugbear when it comes to Ada. For what it's worth, there has been some new life on that front and people are working on improving things. So far it's still very, very early days though. The biggest news so far is Gnoga, a web-socket based, uh, web framework that's usable with Gtk WebViews. It will take awhile, but hopefully this trend will continue and the Ada FOSS community will be able to rouse itself. If you can't tell, I'm not quite ready to count Ada as a lost cause. If it is, and we are looking at running with a new, safe language, at a minimum we shouldn't be forced to take some serious steps back. I'd have loved to see Rust focus on general safety and correctness rather than just memory safety, but it didn't. Losing all that is a rather bitter pill to swallow. "Ironsides..." Totally reasonable, and I think it would be very interesting to see. "Far as Ada vs Rust..." I've been really hoping to find a good comparison for some time now. I know Rust is able to make stronger guarantees about memory than Ada/SPARK can, but it isn't able to handle every case. I'm really curious to see how well Ada/SPARK is able to handle both what Rust can prove, and what it can't. I also don't know if Rust offers any more imprecise safety nets for the cases it can't prove. Finally, I know nothing about how Rust handles concurrency, so that would be another great comparison to see. "Note: You should get a real account if you're a programmer AND know Ada/SPARK. Seriously under-represented here." I might. The plan was for this to be a rather temporary account, but it seems to have stuck.
bluejekyll 11y ago
I'm working on something: https://github.com/bluejekyll/trust-dns https://github.com/bluejekyll/trust-dns I'm in the midst of implementing DNSSec right now, I've got RRSIG and DNSKEY validation back to the root now. I'm working on negative query validation right now, NSEC and NSEC3. Maybe a new release in a few weeks after that is supported.
- grok2 11y ago
  Having used Rust for this, what are your thoughts about how Rust fares for such tasks -- is coding this in Rust better than using C; do you think you are having fewer problems in the end-product as compared to if you had used C. What are the kinds of issues that annoy you about Rust for this? Does the promise of Rust hold up? I am trying to see if I should use Rust for network programming and want to find out how Rust feels for these kinds of projects.
  - bluejekyll 11y ago
    Honestly, comparing (safe) Rust to C is like comparing Java to C. Rust is a higher level language than C, so writing in Rust means (especially for security and network programming) means that I don't have to worry about initialization of memory, or allocation, or deallocation. That's where all my bugs came from in C. In terms of use, I'd say there are still gaps in the number of available libraries, and features of those. I had to add some options to the OpenSSL Rust interface for instance. The non-blocking IO library, mio, is very solid and portable! And I want to play with rotor as a higher level abstraction. If you use Rust instead of C, you will have fewer memory related bugs, and you have more portable code than std C. Rust makes happy low level programmers :)

Interesting. So will this for anyone brave enough to use SPARK and Rust: http://ironsides.martincarlisle.com/ http://ironsides.martincarlisle.com/ IRONSIDES uses SPARK to show freedom of exceptions or single-packet DOS. A translation to Rust would probably preserve most of those properties. I also thought a parallel development between Ada2012/SPARK and Rust would be interesting to see if one set of checkers catch something another misses in same piece of software.

fghfghgfhfg 11y ago
My understanding is that Rust doesn't have so much to offer Ada/SPARK. I haven't looked that hard at Rust though, so maybe I've overlooked some of it's features. You have to jump through the same sort of hoops in Rust as you do C++ to get the sort of basic type safety found in Ada/SPARK. Rust doesn't so much have a focus on safety and correctness in general, as a focus on memory safety. Admittedly, Ada/SPARK doesn't make the kinds of guarantees that Rust does about memory. However, accessibility checks help prevent dangling pointers and the use of memory subpools can avoid the need for explicit frees. Additionally, Ada offers some features like the ability to return a dynamically sized array as if it were on the stack which helps reduce how often memory needs to be manually managed. I believe SPARK may not allow this sort of thing though. I'm also not sure why you would want to abandon the actually verified properties of Ironsides for a hope those properties remained in an unverified port.
- nickpsecurity 11y ago
  "My understanding is that Rust doesn't have so much to offer Ada/SPARK. I haven't looked that hard at Rust though, so maybe I've overlooked some of it's features." I liked the juxtaposition of that haha. It kind of negates anything about Rust in your counterpoint. Your points on Ada/SPARK are still worthwhile. "Ada offers..." No doubt. It was systematically designed to reduce the existence or impact of flaws throughout software. They kept this up in extensions. SPARK straight up proves the absence of them in a subset. So, it's what my gold standard is for safe, systems programming. Rust is the newcomer with interesting additions inspired by safer-than-C imperative and functional languages. It's confusing scheme for memory and concurrency protection is said to be quite effective. It might end up better than Ada over time or just different tradeoffs. The important thing, though, is that it has what Ada/SPARK will likely never have: large-scale adoption with uptake by big companies and users who will add to its ecosystem. Ada FOSS community is barely there with biggest deliverables coming from AdaCore. Remember Gabriel's Worse is Better? Real lesson of it is certain things get adoption better than others. Best to bet on them. Rust is in that category a bit but with Right Thing elements. So, it's worth investing in for long-term benefit of IT. "I'm also not sure why you would want to abandon the actually verified properties of Ironsides for a hope those properties remained in an unverified port." I'm not necessarily suggesting that. There's a reason that OpenBSD and some proprietary vendors keep their system working on several compilers. There's a reason NASA project here used 4 static analysis tools. There's a reason B3/A1 systems kept detailed, formal specs side-by-side with code with both checked. The reason is that different tools catch different types of problems. Further, a problem detected in one might apply to the other. Now, a semantic difference exists between Ada/SPARK and Rust. Yet, there's usually a subset and/or style one can use where results from one about memory or control issues will apply to the other. So, I said do it in parallel: both Ada/SPARK mix and Rust. It displays how each language handles the problem. It let's the analysis tools of each check it for problems that might exist in both. Tool version of many eyeballs except works consistently. ;) It also means that compiler optimization problems in one might not affect an other. Can help with hotfixes while compiler team develops guidance or patches. Also, provides two implementations that can help with adoption and support. There's an issue of maintaining parity but the simpler version is write it in Ada/SPARK w/ Rust release getting uptake. That's the lines I was thinking on. Rust is popular and better than usual. Ada is equal or better in capabilities but not going anywhere. Leverage both to get benefits of both maybe defaulting on Rust release for adoption. Far as Ada vs Rust, I'd like a less biased party that knows Rust's protections and features through and through to do a comparison for me. I have a reference listing each issue Ada tackles and how. I probably can dig up one for SPARK 2014, too. I would love to see what mainstream answer to Ada can do vs the baseline it created. Note: You should get a real account if you're a programmer AND know Ada/SPARK. Seriously under-represented here.
  - fghfghgfhfg 11y ago
    "I liked the juxtaposition of that haha. It kind of negates anything about Rust in your counterpoint." I almost removed that at the end. I wasn't trying to say much about Rust except that it wasn't predicated on this idea of quickly spinning up new, conceptual types with specific constraints like Ada/SPARK. That sort of thing is really either infused throughout a language, or it isn't used. It doesn't take a great deal of familiarity to see that much. Actually, just for this response I went and looked into it a little more. Rust has a tiny bit of syntax sugar for creating structs with positional members. So, you can at least wrap things in a struct a little bit easier than in C++, as you don't need to name the internal value. That's really not enough. Really I mostly wanted to show that Ada also has some means of helping with memory safety - while also being focused on safety/correctness in general. I suppose on that front (and while I'm pushing Ada anyway) I should also mention Ada has a built-in concurrency model, although I suspect you may already be aware of this. "Ada FOSS community is barely there with biggest deliverables coming from AdaCore." Yeah, this is the biggest bugbear when it comes to Ada. For what it's worth, there has been some new life on that front and people are working on improving things. So far it's still very, very early days though. The biggest news so far is Gnoga, a web-socket based, uh, web framework that's usable with Gtk WebViews. It will take awhile, but hopefully this trend will continue and the Ada FOSS community will be able to rouse itself. If you can't tell, I'm not quite ready to count Ada as a lost cause. If it is, and we are looking at running with a new, safe language, at a minimum we shouldn't be forced to take some serious steps back. I'd have loved to see Rust focus on general safety and correctness rather than just memory safety, but it didn't. Losing all that is a rather bitter pill to swallow. "Ironsides..." Totally reasonable, and I think it would be very interesting to see. "Far as Ada vs Rust..." I've been really hoping to find a good comparison for some time now. I know Rust is able to make stronger guarantees about memory than Ada/SPARK can, but it isn't able to handle every case. I'm really curious to see how well Ada/SPARK is able to handle both what Rust can prove, and what it can't. I also don't know if Rust offers any more imprecise safety nets for the cases it can't prove. Finally, I know nothing about how Rust handles concurrency, so that would be another great comparison to see. "Note: You should get a real account if you're a programmer AND know Ada/SPARK. Seriously under-represented here." I might. The plan was for this to be a rather temporary account, but it seems to have stuck.

bluejekyll 11y ago

I'm working on something: https://github.com/bluejekyll/trust-dns https://github.com/bluejekyll/trust-dns I'm in the midst of implementing DNSSec right now, I've got RRSIG and DNSKEY validation back to the root now. I'm working on negative query validation right now, NSEC and NSEC3. Maybe a new release in a few weeks after that is supported.

grok2 11y ago
Having used Rust for this, what are your thoughts about how Rust fares for such tasks -- is coding this in Rust better than using C; do you think you are having fewer problems in the end-product as compared to if you had used C. What are the kinds of issues that annoy you about Rust for this? Does the promise of Rust hold up? I am trying to see if I should use Rust for network programming and want to find out how Rust feels for these kinds of projects.
- bluejekyll 11y ago
  Honestly, comparing (safe) Rust to C is like comparing Java to C. Rust is a higher level language than C, so writing in Rust means (especially for security and network programming) means that I don't have to worry about initialization of memory, or allocation, or deallocation. That's where all my bugs came from in C. In terms of use, I'd say there are still gaps in the number of available libraries, and features of those. I had to add some options to the OpenSSL Rust interface for instance. The non-blocking IO library, mio, is very solid and portable! And I want to play with rotor as a higher level abstraction. If you use Rust instead of C, you will have fewer memory related bugs, and you have more portable code than std C. Rust makes happy low level programmers :)