vault backup: 2025-02-20 15:48:21
This commit is contained in:
parent
680fb334ac
commit
7ed288dd9c
22
.obsidian/workspace.json
vendored
22
.obsidian/workspace.json
vendored
@ -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",
|
||||
|
@ -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"?
|
||||
- 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?
|
||||
|
33
Software Engineering/Meeting.md
Normal file
33
Software Engineering/Meeting.md
Normal file
@ -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.
|
Loading…
x
Reference in New Issue
Block a user