From 7ed288dd9cf8fe609cb4d81d6d0996862cf27c73 Mon Sep 17 00:00:00 2001 From: Boyan Date: Thu, 20 Feb 2025 15:48:21 +0100 Subject: [PATCH] vault backup: 2025-02-20 15:48:21 --- .obsidian/workspace.json | 22 ++++++++++++--- Software Engineering/Initial Questions.md | 11 ++++---- Software Engineering/Meeting.md | 33 +++++++++++++++++++++++ 3 files changed, 58 insertions(+), 8 deletions(-) create mode 100644 Software Engineering/Meeting.md diff --git a/.obsidian/workspace.json b/.obsidian/workspace.json index f4c8470..4fd86fd 100644 --- a/.obsidian/workspace.json +++ b/.obsidian/workspace.json @@ -10,6 +10,20 @@ { "id": "fcc28e70ad8acbd2", "type": "leaf", + "state": { + "type": "markdown", + "state": { + "file": "Software Engineering/Meeting.md", + "mode": "source", + "source": false + }, + "icon": "lucide-file", + "title": "Meeting" + } + }, + { + "id": "2768622d9c36a711", + "type": "leaf", "state": { "type": "markdown", "state": { @@ -21,7 +35,8 @@ "title": "Initial Questions" } } - ] + ], + "currentTab": 1 } ], "direction": "vertical" @@ -199,14 +214,15 @@ "omnisearch:Omnisearch": false } }, - "active": "fcc28e70ad8acbd2", + "active": "2768622d9c36a711", "lastOpenFiles": [ + "Software Engineering/Meeting.md", + "Software Engineering/Initial Questions.md", "Software Engineering/TA Meeting 1.md", "Extracurricular/Misc/Plan.md", "Extracurricular/Misc/Proposed Routine Plan.canvas", "Extracurricular/Misc/Ideas.md", "Extracurricular/Circuitree/Antenna Building/Idea and proposed timeline.md", - "Software Engineering/Initial Questions.md", "Extracurricular/Circuitree/Antenna Building/Untitled", "Extracurricular/Circuitree/Antenna Building", "Functional Programming/Proofs.md", diff --git a/Software Engineering/Initial Questions.md b/Software Engineering/Initial Questions.md index ac51577..1adfd41 100644 --- a/Software Engineering/Initial Questions.md +++ b/Software Engineering/Initial Questions.md @@ -1,23 +1,24 @@ ### Logistics -- Will we have access to an overview of the project roadmap, including deliverables? +- Will we have access to an overview of the project roadmap, including deliverables?\ +> No. It is a research project, hence no deliverables and such. - Do you need us to use specific project management tools (e.g. GitHub, Jira, etc.)? - How often are you available? Is it possible to have weekly progress reports? +> Every week is good. ### Formal Verification - What is the expected level of background in Coq or formal methods? +> It's possible to catch up to speed in a couple of months - Can you explain the process by which a smart contract's safety properties will be validated formally? - Are there any existing case studies or example proofs we might refer to for a better understanding of the expected output? - +> - Define the contract verification criteria ### Project scope clarifications - Among the seven smart contracts being verified, which ones do you expect us to work on, and why those? - Which technologies are we going to be introduced to, if any? Will we have access to guides for Coq and Solidity? - How do you envision the high-level Coq framework integrating with existing Solidity projects? - - ### Optional - How much of the formal verification process will be based on axioms versus fully constructive proofs? - Could you elaborate on the notion of “high-level primitives” (e.g., identity, item, property) and how flexible they need to be for different types of contracts? -- "real numbers and integer approximations"? \ No newline at end of file +- Could you specify what you mean by "real numbers and integer approximations"? Is it related to precision with math? How does that impact the security of a smart contract? Practical example? diff --git a/Software Engineering/Meeting.md b/Software Engineering/Meeting.md new file mode 100644 index 0000000..238c748 --- /dev/null +++ b/Software Engineering/Meeting.md @@ -0,0 +1,33 @@ +## Intro +- Formalland 2 years old +- Formal verification for code, proofs +- Find a way to fully specify smart contracts +- Formal verification as means of security (no bugs -> no stealing) + - Alternatives include: + - Testing (Unit, Value) + - Human expertise + - Quite niche in the field of computer science +- We can be sure that the program follows intended behavior after verification + + +## Smart contracts +- Notion of users +- Admin - owner +- We need to look through some examples [here](https://formal.land/docs/tools/coq-of-solidity/specification-project) to get a feel for them. + - Motivated by bugs [listed here](https://github.com/kadenzipfel/smart-contract-vulnerabilities) + +### Example of Smart Contract +- Stablecoins (USDC) + - Possible specification(?) is to state that the amount of coins is fixed + +## Work +- Solidity +- VSC online + +### Questions during the meeting +- What is the difference between a user and an admin in the context of smart contracts? + +- You mentioned that one possible specification is to state that the amount of coins is fixed. How does that relate to formal verification? To our project? + +- Is the idea to design a DSL? Could you elaborate on the specifics? Do you have a write-up about it or do we need to come up with it? +> Yes. We want to simplify formal verification of smart contracts by creating a DSL. \ No newline at end of file