search

use-ink / ink

Polkadot's ink! to write smart contracts.
https://use.ink
Apache License 2.0
1.35k stars 426 forks source link

Non-Turing-complete subset #295

Open apopiak opened 4 years ago

apopiak commented 4 years ago

As discussed at sub0.1 it would be very useful to be able to write ink contracts in a non-Turing-complete subset that then allows for predictable use of and maybe automatic calculation of resources.

Robbepop commented 4 years ago

Thank you for creating the issue. As soon as we have proper tooling support for checking this we should even make this a default configuration where users can opt out of this check with some annotations for their particular method or implementation.

To implement this check, however, we need Wasm introspection. So we cannot really implement this check on the ink! side but need to provide tools that can check for touring incompleteness on the Wasm level. The ink! side can use this check information if restored into the metadata file and read back into ink!.

Demi-Marie commented 4 years ago

Could this be implemented at the Rust level as a purely syntactic check?

Robbepop commented 4 years ago

Could this be implemented at the Rust level as a purely syntactic check?

I don't think so but happy to be disproven.

apopiak commented 4 years ago

If you white-list syntax and operations it should be possible (though possibly not very useful), no?

Robbepop commented 4 years ago

Could work but not sure how this would work in the presence of Rust macros. We could of course also black-list macro usage but isnt't this getting a bit too restrictive then? Also what about functions that might be turing complete? It is a difficult topic imo but I think if we have tooling support for Wasm introspection available during macro resolution we can tackle this.

athei commented 4 years ago

Maybe it is worth looking at eBPF as they are doing something similar. It is an in-kernel VM (Linux) that is targeted by a LLVM backend. They statically verify termination and other properties. They do the verification on the bytecode level of course. Last time I checked they simply relied on LLVM loop unrolling and statically verified that no code is visted twice. Could be wrong here. That is just from memory. However, they still do not allow non-root users to load eBPF programs into the kernel. I guess that is for a reason (but could be mostly about in-kernel interfaces and not the code execution).

More information: https://lwn.net/Kernel/Index/#Berkeley_Packet_Filter

Demi-Marie commented 4 years ago

Another massive advantage of a non-Turing-complete subset is push-button verification: since the maximum path length is bounded above, an SMT solver can be used to verify properties of the code.