Byont-Ventures / smart-contract-analysis-tools

0 stars 1 forks source link

[Ready] Documentation and setup for blog #47

Closed enzoevers closed 1 year ago

enzoevers commented 1 year ago

It's this document: https://github.com/Byont-Ventures/smart-contract-analysis-tools/blob/41-research-how-the-different-tools-deal-with-external-calls-during-analysis/docs/analysis-techniques.md

jasperverbeet commented 1 year ago

I asked chat gtp to write an introduction to the analysis techniques, here are the 2 options:

This article discusses various analysis techniques that can be used to ensure the quality and correctness of code. The techniques covered include unit testing, fuzzing (property testing), automated testing, Satisfiable Modulo Theory (SMT), symbolic execution, static analysis, and formal verification. The article also discusses how the Byont project utilizes these techniques. Each technique is described in detail, including examples and any limitations or considerations. The article concludes with a list of additional sources for further reading on the topic.

and

This article covers various techniques for analyzing and testing code, including unit testing, fuzzing, automated testing, Satisfiable Modulo Theory (SMT), symbolic execution, static analysis, and formal verification. We'll go over each technique in detail and provide examples and considerations for each. We'll also discuss how the Byont project uses these techniques. Whether you're a seasoned developer or just starting out, there's something in this article for you. Get ready to take your code to the next level!

Vitality-Booster commented 1 year ago

1) Analysis techniques of what? The context a little unclear when I began reading the file. It can be understood from the repository it is in, but I would suggest adding small intro for the document, 2-3 lines would be enough. If you want to make it a blog, then definitely make an introduction.

2) A small tip: it is better to avoid pronouns. It's difficult, but that way the article sounds more professional in a sense.

3) Fuzzing: a) "So now you really need to think of what the behavior is instead of what the result should be. " sounds a bit unclear and "complex". Suggestion: "This kind of test is aimed more at checking the behavior of the function, rather than its output". Something like that. b) "Fuzzing, however, still is only running unit tests." not clear what it means, seems like in this context "unit tests" are seen as something bad/inefficient (?), but I don't why, I think it'd be better to include some more context there.

4) Can we do better? a) Also to make the article look more professional, try to avoid "interacting with a reader". Example there: "Great!" and "Not so great!". I would suggest trying to avoid that.

5) Automated testing a) Check everything with Grammarly, as there are some typos here and there. Example: "This can either the be actual source code ... ." b) "For these techniques, the user has to define a model of how to design works (the design, not the code)." Design works? I didn't understand that, could you elaborate on that? c) Could you in the second paragraph, maybe, reference an article that shows a difference between automated and non-automated verifications? Or maybe elaborate on that more, because I'm still a bit confused how it works with this "design" thingy that I'm also confused with. d) "... the model and the properties and check if they can be satisfied" what exactly can be satisfied there? I'm confused there as well, honestly. e) The part about SMT and Symbolic execution in this chapter sounds pretty good to me.

6) Satisfiable Modulo Theory (SMT) a) "Note that the assumptions and requirements can originate from knowledge about the system in which the function is used, while the function itself doesn't have this knowledge explicitly. The function might be fine when used in the system, but not when used as a self-containing function." I think I understand what you mean there, but I'm not sure that I understood why you included that. Try to explain the reason you mentioned that. Example: "So, it is better to write self-containing functions for SMT". Or something like that. b) "if the requirement (a + b > 100) can hold at al." hold what? Or maybe that some sort phrase that I don't know. But it is unclear for me. c) "Running this in the online tool results in the following output. Saying that if a = 16 and b = 85 that all constraints are met (which is true since 16 + 85 = 101 > 100)." Do you mean in the first sentence that the code below is the output? If yes, then I would after the first sentence put the code and then beneath the code mention: "This code means that f a = 16 and b = 85 that all constraints are met (which is true since 16 + 85 = 101 > 100)." d) The question for the whole z3. Does it mean that in the output it will only tell if the last "assert" is resulting in something or not? Or maybe, with every assert it limits the values that it can use, until there are no more values that satisfies all the asserts and then it sends "unsat" or if there are no more asserts that limit the values it just shows the first situation where all the requirements are met? Maybe, you could explain this flow a bit more in depth. (UPD: was kind of explained in 6.1, but maybe it would be good to also mention here that this question is explained further).

7) Symbolic execution a) "One of the things that are done to reduce the state-space and resource usage is to prune uninteresting states. Pruning was briefly mentioned in the symbolic execution example." Add a link to a good article there or maybe try to explain it yourself, but don't leave just like that. b) In 6.2 in the 3rd paragraph you mention "state-space-explosion", then in the 4th one you tell about "pruning" and in the 5th you return back to the "state-space-explosion". Firstly, finish one topic, then switch to the other one. c) The last paragraph in 6.6. i) Firstly, it is not clear why the tool could return a random value or give up (is it due to the tool or because of the fact that we don't know the function code). ii) Secondly, it is not clear why you mentioned that. It looks more like a random fact. I would suggest in 6.2 say in the beginning: "The example we used is very simple, but what if a more difficult function is tested with Symbolic execution? There are some limits to what you can do: /n 1. Recursive functions and loops. ... /n 2. [something here] /n ... /n 4. External functions. ...". Something like that.

8) Static analysis a) "(be it with symbolic values)" sounds a bit weird and a bit unclear. b) "contributing to a bug in the code" also sounds a bit weird. Maybe, better "leading to / resulting into a bug". c) "check if an external call has to be called, only after the external call" I guess you meant "only after the value is updated". d) "This is because static analysis can be used to get a better picture of the whole code with all its dependencies." why, is it taken for granted? Better to have a link that explains that or your own explanation. I think that this part "Meaning that branches that are not interacting with the state variables can be pruned earlier for example." doesn't explain why static analysis gives a broader picture of the code.

More general tips:

1) Try to sound more professional. Avoid pronouns and "interaction with a reader".
2) Sometimes your article looks like a bunch of facts that are not connected to each other and because of that sometimes I (as a reader) do not understand what is the point of some information or what you are trying to say. Try to make the article fluently and logically go from one point to another.
3) Sometimes also you don't explain enough. You just briefly mention something and move to the other topic. If you just don't want this article to focus on these parts, but you think they are worth mentioning, then just give a source link where people could learn more about the topic. Or you can try to explain yourself, but it is hard to explain some aspect, when you don't want to focus on it too much.
4) Sometimes your language is also hard to understand. I don't know how to help with, just ask for feedback and learn by trial-and-error.

Note: things I mention in general tips, I sometimes pointed out to it earlier, but not everywhere, so you will need to find out some stuff on your own.

Hopefully, that doesn't sound too harsh and nice job for trying writing an article :)

jasperverbeet commented 1 year ago

@enzoevers @Vitality-Booster both very well done! Enzo very nice, interesting and on-topic article. And Vitali thanks for your amazing feedback. πŸ’ͺ🏼πŸ’ͺ🏼 keep it up guys.

jasperverbeet commented 1 year ago

Also @enzoevers you're allowed to give yourself credit in the introduction by telling that you've researched and worked with all these tools. If you choose not to mention it we'll probably do it when posting in on our socials anywhere πŸ™ŒπŸΌ. Up to you...

enzoevers commented 1 year ago

@Vitality-Booster Thanks for the detailed feedback. It's really useful.

enzoevers commented 1 year ago

@SebastiaanCrisan I see that there are quite some consecutive approves from you. Is this because you are looking at each commit individually? If so, I think it is best to look at the changes of a couple of commits together after some time to save doing double work and to see the changes in the bigger picture.

Showing only a selection of commits can be done when being in the "Files changed" tab and then going to the "Changes from ..." drop-down menu that is just above the list with all the files.

Just saying this as a tip. But thanks for the help with the reviews c: