<p>This is a very broad question but here's what I think regarding this topic.</p>
<p><em><strong>Without any of the benefits of hindsight, are there reasons why the exploit would have been less likely to occur in Plutus on Cardano?</strong></em></p>
<p>First of all, this could have happened on Cardano too. As Charles said in his recent update:</p>
<blockquote>
<p>This is not to say that hacks won't happen on Cardano, it will!
(...)
The hacks will occur in uncertified software. Applications that are not rigorously debugged or checked.
(...)
You can't control people maliciously or incompetently writing software that can create problems.
But the existence of certified software against known standards and auditing means that the consumer can have a visual representation (...) that demonstartes the difference between something that is known and reliable and something that is unknown.</p>
</blockquote>
<p>See: <a href="https://youtu.be/xSXSZ5xLpYI?t=665" rel="nofollow noreferrer">https://youtu.be/xSXSZ5xLpYI?t=665</a></p>
<p>What this essentially means is that a similar exploit could happen on Cardano, but it is less likely for certified smart contracts that have been audited. This will not give 100% guarantee that there are no vulnerabilities in the contract. Some vulnerability may be missed in the audit too, but the risk can be greatly reduced.</p>
<p><em><strong>Do Plutus developers also need to learn from these lessons or are they specific to Solidity?</strong></em></p>
<p>I'm no expert when it comes to cross chain relay contracts, but I would answer this question with <em>yes</em>. It's always good to know about possible vulnerabilities and if you ever come across some Plutus code that makes calls to other smart contracts, the polygon hack is something to remember: <em>&quot;Are there any special contracts that I should not be able to call here?&quot;</em>. Knowing about these things can make you write better and more secure code.</p>

CC BY-SA 4.0
2021-08-13T11:51:12.760Z
It was those words from Charles' that prompted me to ask the question.

There is a strong narrative in the community that Cardano smart contracts are going to be more secure. Given that solidity code could also be audited, I’m looking for specific evidence that may support the increased security narrative (e.g. tooling).

Otherwise there is perhaps a risk that the increased complexity/lack of familiarity with functional programming could actually make bugs more common on the [The Island](https://www.youtube.com/watch?v=k8a6tX53YPs&t=399s).
isedwards
CC BY-SA 4.0
2021-08-13T12:01:26.600Z
Haskell is a functional programming language, which is well-suited for high-assurance code and programs that require a high degree of formal verification because every line of code can be mathematically proven to be correct. This is one of the main advantages Plutus smart contracts have in comparison to e.g. Solidity. However, there is a difference between mathematically correct and secure. Plutus can't protect you from making mistakes like getting your access rights wrong as in the polygon example.
eddex
CC BY-SA 4.0
2021-08-13T10:45:53.830Z
2021-08-13T10:45:53.830Z
eddex
<p>[<strong>In short</strong>]</p>
<p>&quot;Things can go wrong in any software&quot; is a statement that misses a mammoth fact. The probability of occurrence can vary on an astronomical scale, like the probability of a bug in a Javascript program( written by me in college) and the code driving the Curiosity rover. There have been bugs even in spacefaring vehicles that had caused catastrophic accidents like thee <a href="https://www-users.cse.umn.edu/%7Earnold/disasters/ariane5rep.html" rel="nofollow noreferrer">Flight 501 Failure</a>. It may not be prudent to compare them at any level. Cardano is written in a Functional Programming language, Haskell, which has existed in the academic world for 30 years. The functional programming paradigm prevents [make it impossible] for programmers to make stupid mistakes and, on top of it, adds formal verification that makes the software space grade. Therefore if we have to follow the human scale and not some astronomical scale, we can say Cardano will not face hacks like what these mushroom networks face.</p>
<p>[<strong>In Detail</strong>]</p>
<p>The piece of the code from the Poly Network which had the vulnerability is referenced below.</p>
<p><a href="https://i.sstatic.net/Tu7Sd.jpg" rel="nofollow noreferrer"><img src="https://i.sstatic.net/Tu7Sd.jpg" alt="enter image description here" /></a>
<a href="https://i.sstatic.net/USC5h.jpg" rel="nofollow noreferrer"><img src="https://i.sstatic.net/USC5h.jpg" alt="Vularable part of Poly Code" /></a></p>
<p><a href="https://blocksecteam.medium.com/the-initial-analysis-of-the-polynetwork-hack-270ac6072e2a" rel="nofollow noreferrer">Analysis</a></p>
<p>There are loops, jumps, and variables. The code can exist in various states. And it becomes impossible to test the code in all the possible states. After learning Haskell and Plutus, I can say with certainty loops, backward and forward jumps, and variables are the sources of all problems. Now for any new programmer, these are the first three steps that are taught. When I started learning Haskel, it was unbelievable that it is possible to program without these basic constructs. Haskell was heavily used by the Math community, which defines function as one input that gives one output irrespective of the date, time, or places it is executed. Everyone knows the square root of 2, but try calculating in C/C++/Java, depending on the floating-point implementation in a particular computer, the result varies by tiny amounts. However, due to the compounding effect of software, these tiny changes add up leading to a noticeable difference downstream. People working in Digital Signal Processing can vouch will vouch for this issue. Like the duration of a second determined by the pendulum clock with a temperature change.</p>
<p>Haskell is based on purity and has no variables and loops. It aims to achieve a lookup table-like behavior in which the values are calculated and pre-stored. Lookup table-like behavior prevents change in output due to state change. The functions are written in Haskell behave like mathematical functions. It goes to great lengths to achieve purity resulting in deterministic behavior. For example, see the following code<a href="https://medium.com/@fabian.schneider/functional-programming-and-formal-software-verification-for-non-industry-applications-fefa24371856#_ftn2" rel="nofollow noreferrer">Take From</a></p>
<pre><code>function main():
print assemble(3)
function assemble(x):
  var y = 0
  var s = “”
  do until (y &gt; x)
    s += y++
  loop
  return s
</code></pre>
<p>and same logic implemented in Haskell</p>
<pre><code>main = putStrLn $ assemble 3
assemble 0 = &quot;0&quot;
assemble y = assemble (y-1) ++ show y
</code></pre>
<p>Now it's not easy to appreciate Haskell's clarity unless we understand the type system. In the first code class, most of the languages accept any type of input to function assemble and try to convert to Int for adding and comparing. Haskell, does not allow writing codes without explicit type constraints. Haskell has a robust type system preventing many logical errors so common in languages like python and javascript. Even functions that have to subtract 2 from a given number can be a source of potential mistakes.</p>
<p>Now that's all good. But if there are no checks put in place, even the most saint of a person can become corrupt. Therefore all software is tested to ensure there is no error. The funny part is that it is some software that tests the other software, and the testing software can only generate fixed-size test scenarios. Therefore there is a need to reduce the surface required to test. The surface of testing is reduced by adopting functional programming. The added advantage is that it inherently helps in carrying out what is called &quot;Formal Verification.&quot; Formal verification is an integral step in VLSI chip manufacturing. That is why there are very few &quot;Bugs&quot; in hardware chips. ( Have you ever come across any bug in the Intel I7 processor? now compare it with the number of bugs you had seen in Microsoft windows!!!.)</p>
<blockquote>
<p>Formal Verification is the process of proving the correctness of systems (hardware/software/algorithms) using mathematical methods. Essentially it is used for ensuring, that something (be it a motherboard, a small chip, a library, a whole program, or an operating system) works as expected. For doing so, one formulates the “thing” mathematically, then formulates theorems that should or shouldn’t hold, and finally proves or disproves these theorems in mathematical ways.</p>
<p>When using the process in Software Development, it is often referred to as Formal Software Verification.</p>
</blockquote>
<p>A pedestrian example is the square of an Integer is Integer. Math can prove this. We don't have to try all possible Integers and check that its square is an Integer. Programs that are written in functional languages can be formally verified. Unfortunately, a purely functional program will have no &quot;so-called&quot; side effects like any interaction with the outside world, like reading and writing into a network socket (used in the propagation of blocks in the blockchain). Therefore, Haskell has come up with very clever ways to permit side effects through strictly controlled mechanisms, preventing expansion of the surface required to carry out the testing.</p>
<p>These are some of the mechanisms which Cardano is using to ensure Secure Operation. Charles' Statement, &quot;This is not to say that hacks won't happen on Cardano, it will! &quot; is a fact. Still, comparative probability and the scale of impact on Risk Management are most likely to be astronomically minimal, compared to ad-hoc blockchains mushrooming out in the wild.</p>

CC BY-SA 4.0
2021-08-13T18:19:06.673Z
2021-08-13T18:58:03.540Z
2021-08-13T18:58:03.540Z
raghu
<p>Over on Twitter, @kelvinfichter <a href="https://twitter.com/kelvinfichter/status/1425217046636371969" rel="noreferrer">gave an analysis</a> (included below) of the recent Poly Network hack.</p>
<p><em><strong>Without any of the benefits of hindsight, are there reasons why the exploit would have been less likely to occur in Plutus on Cardano?</strong></em></p>
<blockquote>
<p>Poly has this contract called the <code>EthCrossChainManager</code>. It's basically a privileged contract that has the right to trigger messages from another chain. It's a pretty standard thing for cross-chain projects.</p>
<p>There's this function <code>verifyHeaderAndExecuteTx</code> that anyone can call to execute a cross-chain transaction. Basically it:</p>
<ol>
<li>Verifies that the block header is correct by checking signatures (seems the other chain was a poa sidechain or something) and... then</li>
<li>Checks that the transaction was included within that block with a Merkle proof. Here's the code, it's pretty simple: <a href="https://github.com/polynetwork/eth-contracts/blob/d16252b2b857eecf8e558bd3e1f3bb14cff30e9b/contracts/core/cross_chain_manager/logic/EthCrossChainManager.sol#L127" rel="noreferrer">EthCrossChainManager.sol#L127</a></li>
</ol>
<p>One of the last things the function does is call <code>_executeCrossChainTx</code>, which actually makes the call to the target contract. Here's where the critical flaw sits.</p>
<p>Poly checks that the target is a contract <a href="https://github.com/polynetwork/eth-contracts/blob/d16252b2b857eecf8e558bd3e1f3bb14cff30e9b/contracts/core/cross_chain_manager/logic/EthCrossChainManager.sol#L185" rel="noreferrer">EthCrossChainManager.sol#L185</a>. But Poly forgot to prevent users from calling a very important target... the <code>EthCrossChainData</code> contract: <a href="https://github.com/polynetwork/eth-contracts/blob/master/contracts/core/cross_chain_manager/data/EthCrossChainData.sol" rel="noreferrer">EthCrossChainData.sol</a>.</p>
<p>Why is this target so important? It keeps track of the list of public keys that authenticate data coming from the other chain. If you can modify that list, you don't even need to hack private keys. You just set the public keys to match your own private keys. See here for where that list is tracked: <a href="https://github.com/polynetwork/eth-contracts/blob/d16252b2b857eecf8e558bd3e1f3bb14cff30e9b/contracts/core/cross_chain_manager/data/EthCrossChainData.sol#L22" rel="noreferrer">EthCrossChainData.sol#L22</a>.</p>
<p>So someone realized that they could send an cross-chain message directly to the <code>EthCrossChainData</code> contract.</p>
<p>What good does that do them? Well, guess which contracted owned the EthCrossChainData contract... yep. The <code>EthCrossChainManager</code>. By sending this cross-chain message, the user could trick the <code>EthCrossChainManager</code> into calling the <code>EthCrossChainData</code> contract, passing the <code>onlyOwner</code> check.</p>
<p>Now the user just had to craft the right data to be able to trigger the function that changes the public keys. Link to that function here: <a href="https://github.com/polynetwork/eth-contracts/blob/d16252b2b857eecf8e558bd3e1f3bb14cff30e9b/contracts/core/cross_chain_manager/data/EthCrossChainData.sol#L45" rel="noreferrer">EthCrossChainData.sol#L45</a>.</p>
<p>The only remaining challenge was to figure out how to make the <code>EthCrossChainManager</code> call the right function. Now comes a little bit of complexity around how Solidity picks which function you're trying to call.</p>
<p>The first four bytes of transaction input data is called the &quot;signature hash&quot; or &quot;sighash&quot; for short. It's a short piece of information that tells a Solidity contract what you're trying to do. The sighash of a function is calculated by taking the first four bytes of the hash of &quot;()&quot;.</p>
<p>For example, the sighash of the ERC20 transfer function is the first four bytes of the hash of <code>transfer(address,uint256)</code>. Poly's contract was willing to call <em>any</em> contract. However, it would only call the contract function that corresponded to the following sighash: Errr but wait... <code>_method</code> here was user input.</p>
<p>All the attacker had to do to call the right function was figure out <em>some</em> value for <code>_method</code> that, when combined with those other values and hashed, had the same leading four bytes as the sighash of our target function.</p>
<p>With just a little bit of grinding, you can <em>easily</em> find some input that produces the right sighash. You don't need to find a full hash collision, you're only checking the first four bytes.</p>
<p>So is this theory correct? Well... here's the actual sighash of the target function:</p>
<pre><code>&gt; ethers.utils.id ('putCurEpochConPubKeyBytes(bytes)').slice(0, 10)
'0x41973cd9'`
</code></pre>
<p>And the sighash that the attacker crafted...</p>
<pre><code>&gt; ethers.utils.id ('f1121318093(bytes,bytes,uint64)').slice(0, 10)
'0x41973cd9'
</code></pre>
<p>Fantastic. No private key compromise required! Just craft the right data and boom... the contract will just hack itself!</p>
</blockquote>
<p>The author then goes on to <a href="https://twitter.com/kelvinfichter/status/1425220160814784512" rel="noreferrer">give lessons learned</a>.</p>
<p><em><strong>Do Plutus developers also need to learn from these lessons or are they specific to Solidity?</strong></em></p>
<blockquote>
<p>One of the biggest design lessons that people need to take away from this is: if you have cross-chain relay contracts like this, MAKE SURE THAT THEY CAN'T BE USED TO CALL SPECIAL CONTRACTS.</p>
<p>The <code>EthCrossDomainManager</code> shouldn't have owned the <code>EthCrossDomainData</code> contract. Separate concerns.</p>
<p>If your contract absolutely need to have special privileges like this, make sure that users can't use cross-chain messages to call those special contracts.</p>
<p>And just for good measure, here's the function to trigger a cross-chain message: <a href="https://github.com/polynetwork/eth-contracts/blob/d16252b2b857eecf8e558bd3e1f3bb14cff30e9b/contracts/core/cross_chain_manager/logic/EthCrossChainManager.sol#L91" rel="noreferrer">EthCrossChainManager.sol#L91</a>. Nothing here prevents you from sending a message to the <code>EthCrossChainData</code> contract.</p>
</blockquote>
<p>@kelvinfichter also gives a simplified summary of the attack: <a href="https://twitter.com/kelvinfichter/status/1425290462076747777" rel="noreferrer">https://twitter.com/kelvinfichter/status/1425290462076747777</a></p>

CC BY-SA 4.0
2021-08-20T10:06:43.833Z
Here's a link to Charles Hoskinson talking about the Cardano/Plutus approach back in March 2019: https://youtube.com/watch?v=f-rqaTLwWgs&t=4483s
isedwards
<plutus><ethereum><solidity>
Poly Network attack - lessons for Plutus devs?
# Poly Network attack - lessons for Plutus devs?

(Asked by: username_0 on 2021-08-11)

Over on Twitter, @kelvinfichter gave an analysis (included below) of the recent Poly Network hack.
Without any of the benefits of hindsight, are there reasons why the exploit would have been less likely to occur in Plutus on Cardano?

Poly has this contract called the EthCrossChainManager. It's basically a privileged contract that has the right to trigger messages from another chain. It's a pretty standard thing for cross-chain projects.
There's this function verifyHeaderAndExecuteTx that anyone can call to execute a cross-chain transaction. Basically it:

Verifies that the block header is correct by checking signatures (seems the other chain was a poa sidechain or something) and... then
Checks that the transaction was included within that block with a Merkle proof. Here's the code, it's pretty simple: EthCrossChainManager.sol#L127

One of the last things the function does is call _executeCrossChainTx, which actually makes the call to the target contract. Here's where the critical flaw sits.
Poly checks that the target is a contract EthCrossChainManager.sol#L185. But Poly forgot to prevent users from calling a very important target... the EthCrossChainData contract: EthCrossChainData.sol.
Why is this target so important? It keeps track of the list of public keys that authenticate data coming from the other chain. If you can modify that list, you don't even need to hack private keys. You just set the public keys to match your own private keys. See here for where that list is tracked: EthCrossChainData.sol#L22.
So someone realized that they could send an cross-chain message directly to the EthCrossChainData contract.
What good does that do them? Well, guess which contracted owned the EthCrossChainData contract... yep. The EthCrossChainManager. By sending this cross-chain message, the user could trick the EthCrossChainManager into calling the EthCrossChainData contract, passing the onlyOwner check.
Now the user just had to craft the right data to be able to trigger the function that changes the public keys. Link to that function here: EthCrossChainData.sol#L45.
The only remaining challenge was to figure out how to make the EthCrossChainManager call the right function. Now comes a little bit of complexity around how Solidity picks which function you're trying to call.
The first four bytes of transaction input data is called the "signature hash" or "sighash" for short. It's a short piece of information that tells a Solidity contract what you're trying to do. The sighash of a function is calculated by taking the first four bytes of the hash of "()".
For example, the sighash of the ERC20 transfer function is the first four bytes of the hash of transfer(address,uint256). Poly's contract was willing to call any contract. However, it would only call the contract function that corresponded to the following sighash: Errr but wait... _method here was user input.
All the attacker had to do to call the right function was figure out some value for _method that, when combined with those other values and hashed, had the same leading four bytes as the sighash of our target function.
With just a little bit of grinding, you can easily find some input that produces the right sighash. You don't need to find a full hash collision, you're only checking the first four bytes.
So is this theory correct? Well... here's the actual sighash of the target function:
> ethers.utils.id ('putCurEpochConPubKeyBytes(bytes)').slice(0, 10)
'0x41973cd9'`

And the sighash that the attacker crafted...
> ethers.utils.id ('f1121318093(bytes,bytes,uint64)').slice(0, 10)
'0x41973cd9'

Fantastic. No private key compromise required! Just craft the right data and boom... the contract will just hack itself!

The author then goes on to give lessons learned.
Do Plutus developers also need to learn from these lessons or are they specific to Solidity?

One of the biggest design lessons that people need to take away from this is: if you have cross-chain relay contracts like this, MAKE SURE THAT THEY CAN'T BE USED TO CALL SPECIAL CONTRACTS.
The EthCrossDomainManager shouldn't have owned the EthCrossDomainData contract. Separate concerns.
If your contract absolutely need to have special privileges like this, make sure that users can't use cross-chain messages to call those special contracts.
And just for good measure, here's the function to trigger a cross-chain message: EthCrossChainManager.sol#L91. Nothing here prevents you from sending a message to the EthCrossChainData contract.

@kelvinfichter also gives a simplified summary of the attack: https://twitter.com/kelvinfichter/status/1425290462076747777

**Tags:** plutus, ethereum, solidity
> **Comments:**
> **username_0**: Here's a link to Charles Hoskinson talking about the Cardano/Plutus approach back in March 2019: https://youtube.com/watch?v=f-rqaTLwWgs&t=4483s  

---

## 2 answers

### Answer by username_1 on 2021-08-13. Score: 3 | Accepted answer

This is a very broad question but here's what I think regarding this topic.

***Without any of the benefits of hindsight, are there reasons why the exploit would have been less likely to occur in Plutus on Cardano?***

First of all, this could have happened on Cardano too. As Charles said in his recent update:

> This is not to say that hacks won't happen on Cardano, it will!
> (...)
> The hacks will occur in uncertified software. Applications that are not rigorously debugged or checked.
> (...)
> You can't control people maliciously or incompetently writing software that can create problems.
> But the existence of certified software against known standards and auditing means that the consumer can have a visual representation (...) that demonstartes the difference between something that is known and reliable and something that is unknown.

See: <https://youtu.be/xSXSZ5xLpYI?t=665>

What this essentially means is that a similar exploit could happen on Cardano, but it is less likely for certified smart contracts that have been audited. This will not give 100% guarantee that there are no vulnerabilities in the contract. Some vulnerability may be missed in the audit too, but the risk can be greatly reduced.

***Do Plutus developers also need to learn from these lessons or are they specific to Solidity?***

I'm no expert when it comes to cross chain relay contracts, but I would answer this question with *yes*. It's always good to know about possible vulnerabilities and if you ever come across some Plutus code that makes calls to other smart contracts, the polygon hack is something to remember: *"Are there any special contracts that I should not be able to call here?"*. Knowing about these things can make you write better and more secure code.

> **Comments:**
> **username_0**: It was those words from Charles' that prompted me to ask the question.  There is a strong narrative in the community that Cardano smart contracts are going to be more secure. Given that solidity code could also be audited, I’m looking for specific evidence that may support the increased security narrative (e.g. tooling).  Otherwise there is perhaps a risk that the increased complexity/lack of familiarity with functional programming could actually make bugs more common on the [The Island](https://www.youtube.com/watch?v=k8a6tX53YPs&t=399s).  
> **username_1**: Haskell is a functional programming language, which is well-suited for high-assurance code and programs that require a high degree of formal verification because every line of code can be mathematically proven to be correct. This is one of the main advantages Plutus smart contracts have in comparison to e.g. Solidity. However, there is a difference between mathematically correct and secure. Plutus can't protect you from making mistakes like getting your access rights wrong as in the polygon example.  

---

### Answer by username_2 on 2021-08-13. Score: 3

[In short]
"Things can go wrong in any software" is a statement that misses a mammoth fact. The probability of occurrence can vary on an astronomical scale, like the probability of a bug in a Javascript program( written by me in college) and the code driving the Curiosity rover. There have been bugs even in spacefaring vehicles that had caused catastrophic accidents like thee Flight 501 Failure. It may not be prudent to compare them at any level. Cardano is written in a Functional Programming language, Haskell, which has existed in the academic world for 30 years. The functional programming paradigm prevents [make it impossible] for programmers to make stupid mistakes and, on top of it, adds formal verification that makes the software space grade. Therefore if we have to follow the human scale and not some astronomical scale, we can say Cardano will not face hacks like what these mushroom networks face.
[In Detail]
The piece of the code from the Poly Network which had the vulnerability is referenced below.


Analysis
There are loops, jumps, and variables. The code can exist in various states. And it becomes impossible to test the code in all the possible states. After learning Haskell and Plutus, I can say with certainty loops, backward and forward jumps, and variables are the sources of all problems. Now for any new programmer, these are the first three steps that are taught. When I started learning Haskel, it was unbelievable that it is possible to program without these basic constructs. Haskell was heavily used by the Math community, which defines function as one input that gives one output irrespective of the date, time, or places it is executed. Everyone knows the square root of 2, but try calculating in C/C++/Java, depending on the floating-point implementation in a particular computer, the result varies by tiny amounts. However, due to the compounding effect of software, these tiny changes add up leading to a noticeable difference downstream. People working in Digital Signal Processing can vouch will vouch for this issue. Like the duration of a second determined by the pendulum clock with a temperature change.
Haskell is based on purity and has no variables and loops. It aims to achieve a lookup table-like behavior in which the values are calculated and pre-stored. Lookup table-like behavior prevents change in output due to state change. The functions are written in Haskell behave like mathematical functions. It goes to great lengths to achieve purity resulting in deterministic behavior. For example, see the following codeTake From
function main():
print assemble(3)
function assemble(x):
  var y = 0
  var s = “”
  do until (y > x)
    s += y++
  loop
  return s

and same logic implemented in Haskell
main = putStrLn $ assemble 3
assemble 0 = "0"
assemble y = assemble (y-1) ++ show y

Now it's not easy to appreciate Haskell's clarity unless we understand the type system. In the first code class, most of the languages accept any type of input to function assemble and try to convert to Int for adding and comparing. Haskell, does not allow writing codes without explicit type constraints. Haskell has a robust type system preventing many logical errors so common in languages like python and javascript. Even functions that have to subtract 2 from a given number can be a source of potential mistakes.
Now that's all good. But if there are no checks put in place, even the most saint of a person can become corrupt. Therefore all software is tested to ensure there is no error. The funny part is that it is some software that tests the other software, and the testing software can only generate fixed-size test scenarios. Therefore there is a need to reduce the surface required to test. The surface of testing is reduced by adopting functional programming. The added advantage is that it inherently helps in carrying out what is called "Formal Verification." Formal verification is an integral step in VLSI chip manufacturing. That is why there are very few "Bugs" in hardware chips. ( Have you ever come across any bug in the Intel I7 processor? now compare it with the number of bugs you had seen in Microsoft windows!!!.)

Formal Verification is the process of proving the correctness of systems (hardware/software/algorithms) using mathematical methods. Essentially it is used for ensuring, that something (be it a motherboard, a small chip, a library, a whole program, or an operating system) works as expected. For doing so, one formulates the “thing” mathematically, then formulates theorems that should or shouldn’t hold, and finally proves or disproves these theorems in mathematical ways.
When using the process in Software Development, it is often referred to as Formal Software Verification.

A pedestrian example is the square of an Integer is Integer. Math can prove this. We don't have to try all possible Integers and check that its square is an Integer. Programs that are written in functional languages can be formally verified. Unfortunately, a purely functional program will have no "so-called" side effects like any interaction with the outside world, like reading and writing into a network socket (used in the propagation of blocks in the blockchain). Therefore, Haskell has come up with very clever ways to permit side effects through strictly controlled mechanisms, preventing expansion of the surface required to carry out the testing.
These are some of the mechanisms which Cardano is using to ensure Secure Operation. Charles' Statement, "This is not to say that hacks won't happen on Cardano, it will! " is a fact. Still, comparative probability and the scale of impact on Risk Management are most likely to be astronomically minimal, compared to ad-hoc blockchains mushrooming out in the wild.


---

