Guest Lectures on Static Analysis for Rust: tracking issue

[bhargavbh]

I will be giving a guest lecture on Static Analysis techniques for Rust at the PBA in UCB. You can find the lecture proposal with my ideas here.
Objective is to introduce tools and techniques for static analysis which the students can use in their workflow.

My plan is keep the lecture generic for Rust, while designing assignments/exercises that are specific to Substrate.
The lectures are hands-on with a brief overview of theory and demonstrating usage of tools like MIRAI (abstract interpreter) and Crux-MIR (symbolic execution engine).
Time permitting, I also have ideas for a lecture on Fuzzing with tools like libfuzzer and AFL. We at the foundation have been working on a differential fuzzer for polkadot host.

After discussions with @nukemandan, we felt that FRAME module would be apt for slotting this content. The students would have had enough exposure to substrate. We can design assignments where the student run static analysers (introduced in the lecture) on their pallets to detect panics statically.

As the FRAME module lead @shawntabrizi , how much time do you think can be accommodated for this lecture/s. I could finish the lecture by introducing the assignment, and maybe have async "office-hour" sessions for helping the students.
Since its not part of core curriculum, we can keep the assignment optional without a formal grading process.

Any other suggestion for content/structuring are welcome.

[shawntabrizi]

To be honest, I feel this might be more of an extra "nice-to-have" rather than a core part of the FRAME module. I say that because, its true what you said, we really don't use static analysis much throughout Polkadot / Substrate at the moment...

I do think the material is interesting, and something even I would want to learn, but its all about a battle for time to teach the material, and not making students stress out from extra work. If there is room for it in the FRAME module, then we can put it in, but I feel at this point we need to play it by ear.

I would be very happy for you to start working on the material and slides, and we can see how to integrate it once it is done.

One other more crazy idea would be to turn this into a recorded video lecture as additional material students (and the rest of the community) can access.

Anyway, +1 on the idea, but I wouldn't necessarily prioritize this over cutting other stuff, or pressuring students too much. Let me know what you think about my feedback.

[nuke-web3]

I agree we have @bhargavbh start work on the lesson(s) and exercise(s) and then decide where it will fit in the timeline. If we try to make this more generic Rust at much as possible, we can have this fit into any place at the PBA and then have some Substrate / FRAME specific content come latter on.

Perhaps as a remote session and/or all packaged in a self-driven learning module and then when you (@bhargavbh and whoever leads this content in the future) are able to join IRL can do a hands-on session building on that. This also might be able to live anytime after we cover some core aspects of Substrate needed to run, perhaps as a way to close the course out around or after XCM.

• How much time do we need for the biggest vision and full scope the content?
• How much time would we need for a minimal complete lecture related to this topic?

[bhargavbh]

Thanks @shawntabrizi @nukemandan for your feedback. Definitely, this content should be seen more of an elective than core part of any module. Its hard to assume that all 80 students are willing to put more effort into learning static analysis (after a gruelling academy), but i think there might be significant fraction if we structure it right.

I am happy to create initial drafts of slides for my lecture and sketch a few exercises. As @nukemandan suggested, we can possibly decouple the lecture and exercise-sessions.
i can work on 1hr lecture generic to rust verification/analysis, and end the lecture by introducing Susbtrate specific assignments. This lecture can be slotted in any of the modules. It will cover the fundamentals without much coding/demo session.
We can then have a hands-on elective session (2-3hrs) to help the students with the exercises (for e.g. the weekend falling within the FRAME module). The objective of this session would be to break the initial barrier when working with new tools, assuming students didn't have the chance to attempt exercise earlier. For students who already attempted, we can help them run it on their pet projects.

TLDR; the lecture would cover the breadth (that everyone attends), and the exercise session dives deep (for those
interested) on MIRAI tool. The durations i mentioned are the minimum for anything meaningful. If there is more time, i can ofcourse cover more breadth in lecture and depth in exercises.
Will get back once i have draft of slides ready in the coming weeks

[bhargavbh]

I have a draft of my slides in bnb/RustStaticAnalysis branch here. It still needs quite a bit of polishing both content wise and formatting, and some conclusion slides.
The content is mostly generic rust verification: intro to formal methods, paints a landscape of available rust tools, and then focuses on Kani (model-checker for Rust) with several demos. If time permits, i can also make a similar deep-dive for MIRAI tool.
I have already designed an exercise where the Kani tool is to be used for verifying SCALE codec, basically the roundtrip property. I am now looking for concrete exercise ideas for application to FRAME. Any leads here would be great. Ideally, i would want to the student to run Kani on the code written by them as part of PBA.

[kianenigma]

@bhargavbh you might want to contribute to the discussion here: paritytech/polkadot-sdk#165

[bhargavbh]

@kianenigma thanks for the pointer. The discussion seems super interesting to me! Will definitely pitch in after digging a bit more into the problem and context.

[nuke-web3]

paritytech/substrate#649 now is looking for a concrete placement in the sequence for the week of the 24th of July. Is there a good opening we can fill in the normal day this week?

As well as the optional workshop that would need to land on Saturday (note that this competes with whatever the assignment is this time that day!) or a weeknight around the social/founders track content that will be happening (that is tracked here)