Hello : or is in terms of Nim-Lang security compared to other languages. we hear a lot about Rust, but I think it's mostly a way of programming that influences security outside of traditional reasons ...
This is a question for information
I'm working in the field and Nim is my "everyday job language". Translation: Nim is considerably less qualified than Ada (much harder to master), Eiffel (unattractive for some other reasons), and even Ocaml (less attractive for multiple reasons), let alone F star (which however is considerably more demanding and more complex plus poorly documented). But Nim is way better qualified than most languages in common use (except a few which are however either JVM or .Net based). Some reasons for that are strong static typing, (albeit still very modest contracts), good readability and a creator/team leader with a healthy mindset and knowledge of and respect for languages like Modula [2|3], Pascal.
One point I'd like to add, although not yet final (more testing required), is that Nim (inter alia and probably most used) translates to C which can be statically and dynamically tested.
For hardcore security jobs I still use Ada, for (rare) GUI jobs I still use FreePascal, for pure crypto jobs like porting or optimizing crypto algos I still use C along with formal modelling, proto verif. and (usually static) analysis.
I'm currently looking closely at the C code Nim generates. I'm not exactly happy because it looks very ugly and seems to occasionally produce, let me word it nicely, strange code and errors in static analysis (might be false positives), that's why I still keep Ada at hand. But if my tests would show that Nim generates reliably error free code (or if the team reacts constructively on eventual criticism) I'll use Nim even for at least some critical jobs.
Note: At least Nim (well, its output) can be statically checked, most languages can't (because there are no tools available), so what I wrote here is not negative as compared to other languages. In fact my impression so far is that Nim is in the top 10% of commonly used languages in terms of safety. So, my testing is not about tearing into Nim but rather about verifying the (positive) impression I've got so far.
Short version/TL;DR: unless it's hardcore jobs (e.g. crypto implementations) Nim is probably the best language in my toolset and the one I like most as well as the most efficient one (in terms of coding time and efforts).
If you want a (premilinary) 1 sentence verdict -> Nim is at least as safe/secure as FreePascal and the C and C++ code it produces is safer/more secure/less buggy than what 98% of developers produce by hand.
thank you Morem
You say less secure than C.
Do you mean to imply that there may be buggers, if that's it it doesn't matter in itself it's perfectible ...
For the moment Nim has helped me by noting and pointing out small errors not functional but easy to generate in C / C++ oh no matter in itself but that I could easily forget, but which when you look carefully should not be produce when writing code. As for the functional it seems more obvious to me but this is only my opinion after 7 months of daily practice.
NO! NOT less secure than C - but less secure than formally verified C. That is a very significant difference.
"Normal" C code, i.e. C code that has not been formally designed and verified is considerably less secure than normal Nim code.
The point is that for C - unlike for most languages - there are static analysis tools avalaible. But those same tools can also be used to verify C code produced by Nim.
For hardcore security jobs I still use Ada, for (rare) GUI jobs I still use FreePascal, for pure crypto jobs like porting or optimizing crypto algos I still use C along with formal modelling, proto verif. and formal (usually static) analysis.
Extremely interesting! Could you give a list of your C formal modelling toolkit / workflow ? And a hint about what kind of common things it flags in Nim generated C code?
Also, since you mentioned using formally verified C for crypto work - is there anything helping with verifying constant time stuff? How useful is everything given that anything practical uses a non-verified compiler somewhere along the high-level -> machine code path?
I'll provide more info once I'm finished doing some verification of Nim C output.
"constant time stuff" - no, I don't know such a tool. Static verifiers are only looking for code correctness, e.g. proper mem. boundaries, reachability, loop invariants, etc. If you want to verify things like constant time operation I'd suggest a modelling tool to check your model ("algorithm"). Note that some MVs can also produce code.
"non-verified compiler" - a) there are some (very few) verified compilers, e.g. CompCert.
The real problem is IMO that static as well as dynamic analyzers are relatively complicated (to use and understand) beasts and to use them properly one must understand quite a bit of formal methods and hence math (e.g. FOL, H3, separation logic) - hence most developers do not use those tools.
One hint I can provide (in terms of easy to use verifiers) is facebooks "infer" tool. Be aware though that infer is rather limited, but it's very easy to use and it seems to catch at least the more common (albeit simple) errors.
P.S. For a list of tools (of very diverse quality and complexity) have a look at the awesome static verifier list at github.
For the reference: Awesome Static Analysis
Yes, that's the list I meant. Thanks.
Note however that that list is extremely "generous" and most entries are just more or less reasonable linters rather than static analyzers/verifiers.
YAY! That's extremely good news. Thanks a lot!
I particularly love to see full H3 - incl. 'invariant'. Are there also plans to provide quantors ('forall', 'exists' (plus negation))? Even hotter: Are there plans to provide a compile time interface to Z3? I'm asking because that would be the "sweet spot" in terms of the least work for the Nim team while providing full formal capabilities for those (probably rather few) Nim developers who need full formal verification, some kind of transfer to/from model checkers, etc.
Last but not least, having some capabilities and/or interface to formal analysis would (IMO) pretty much close the gap between Nim and Ada+Spark plus it would open the door to (step by step) have Nim's stdlib and some major Nim libs fully verified. That plus the fact that Nim, while (still) lacking some of Ada's strengths, also has some strengths that Ada does not have (and is extremely unlikely to ever get) could make Nim preferrable over Ada.
I'm really enchanted by the news. Thanks so much @Araq and Nim team! [pls. imagine a "heart" icon here which to make/insert I'm too clueless]
Are there also plans to provide quantors ('forall', 'exists' (plus negation))? Even hotter: Are there plans to provide a compile time interface to Z3? I'm asking because that would be the "sweet spot" in terms of the least work for the Nim team while providing full formal capabilities for those (probably rather few) Nim developers who need full formal verification, some kind of transfer to/from model checkers, etc.
Quantors are coming and so is negation. We also attach pre- and postconditions to proc types so that method and function pointers work. And the analysis is modular, it doesn't look inside proc bodies. We use the Z3 nimble package to interface with it, there is no "compile time interface to Z3" though as I have no idea what that would look like. We strive to map large portions of Nim to Z3 though including floating point and unsigned math.
Can we have a roadmap for static analysis in Nim? Perhaps during the Nim Online Conference?
Is drnim seen as a complement to nim compiler type checking, trying to balance speed of compilation and type checks in the compiler, with for more deep static analysis the developer would decide to delegate to drnim before integration, for instance?
Static analysis can be understood with a very broad scope, some even including source pretty printers into the domain (see previous Awesome list). Purists will say that the real goal is to find bugs before they occur when the code is executed. Where drnim will stand?
Will there be a way to extend drnim with Z3 constraints/rules/nim code to add checks?
Is drnim seen as a complement to nim compiler type checking, trying to balance speed of compilation and type checks in the compiler, with for more deep static analysis the developer would decide to delegate to drnim before integration, for instance?
That pretty much nails it.
Where drnim will stand?
drnim focusses on verification via Hoare Triples and focusses on:
Nim's effect .tag system can probably be replaced by something more powerful/useful too with this technology.