draft: Project-Based Learning in Software Modelling.

[aleeusgr]

PBL:

Project Based Learning (PBL) experience is a self-sovereign teaching method in which the self learns by actively engaging in real-world and personally meaningful projects.

Title: “A Step-by-Step Guide to Conducting Formal Verification of a Software Product”

dApp Certification on Cardano PBL plan

[aleeusgr]

Documentation review

Cardano Engineering Handbook

Audit/evaluation process is described: https://www.commoncriteriaportal.org/cc/index.cfm

https://github.com/cardano-foundation/CIPs

CIP-52 describes the audit process in general.
CIP-96 describes the way to store and present certification information to all stakeholders.
CIP-72 describes a standardised method for dApp developers to register their dApp(s) on-chain and for users to verify the claims made by dApp developers.

https://en.wikipedia.org/wiki/Requirements_analysis

https://iohk.io/en/blog/posts/2021/09/22/bringing-certified-dapps-to-cardano/
https://iohk.io/en/research/library/papers/translation-certification-for-smart-contracts-extended-abstract/

[aleeusgr]

a chunk:

As Cardano Builders our primary responsibility is to ensure that our users' data, transactions, and digital assets are secure. We emphasize the importance of risk management and security measures to protect the assets from potential threats such as theft, fraud, or unauthorized access. To reduce such risks controls must be imposed on the software artifacts we produce as well as on the process by which we produce these artifacts.

Audit is one such control. An audit is a comprehensive investigation of a DApp that provides an in-depth analysis on bugs, vulnerabilities, code quality and correctness of implementation.
The process of audit on Cardano is described in CIP-52, with additional information available through CIP-72, CIP-96 and articles published on IOHK.io. CIP-52 recommends that a developer should contact an auditor when they have a final working version of a DApp or fragment of a DApp that they want to have audited. It is also recommended to reach out to the potential auditor as early as possible so as to mitigate any design issues which may be very hard if not impossible to fix.

Audit process on Cardano is modeled after the Common Criteria. Common Criteria (CC) is an international standard for computer security certification, developed to ensure that products and systems meet a pre-defined security standard for government deployments. It is a framework in which computer system users can specify their security functional requirements (SFRs) and security functional assurance requirements (SARs) using Protection Profiles (PPs). CC certification is given to security products that have successfully passed the testing and Common Criteria evaluation performed by an accredited Testing Laboratory.

[aleeusgr]

Review in 2025

[aleeusgr]

The top-level design goals were as follows:

Soundness. Verification results should be sound—that is, trustworthy for all compilers and target machines.
Sufficient completeness. Verification of non-trivial properties should offer a tolerably low false-alarm rate.
Formality. The language should be amenable to the development of an unambiguous formal definition.
Scalability. Verification should scale to industrial code bases in reasonable time.
Modularity. Verification of incomplete programs should be possible during their development.
Expressiveness. The language should be usable for building embedded, real-time, and critical software systems, not limited to "toy" examples. The verification system should allow the specification of non-trivial correctness properties, not just a list of "common errors."

https://m-cacm.acm.org/magazines/2024/3/280078-co-developing-programs-and-their-proof-of-correctness/fulltext