The Anoma Virtual Machine (avm) is part of a conceptual tool chest for reasoning about decentralized distributed applications (ddapps) whose state is curated by an Anoma controller via resource commitments and nullifiers. In one sentence, ddapps are modelled as objects that run on the avm in analogy to how applications run on a computing device.
The three main ideas are the following: (1) messages between objects and object state are represented as resources (messages and state as resources), (2) messages are processed during execution of corresponding transactions (transacting as computing), and (3) all inputs from users and other principal agents are submitted as part of intents and transactions (interaction logs as parameters). In one sentence, each avm instance is a fully deterministic systems that is driven by decisions of users and other principal actors that are interested in state changes, either fully specified or expressed as an intent.
This paper focuses on the single controller case. The cross-controller case is covered if you assume that object state is chimera state or you assume that each method invocation of an object can be handled by one controller. For the true cross-controller case, we face the usual issue that we cannot have true atomicity (but must “fake” it, even if Herlihy got away omitting this detail in the title of his paper Atomic cross-chain swaps, because the idea of chimera chains was not yet on ppl’s radar[1]).
Thank you for the updated draft! I’ve reviewed in moderate detail and left line-specific comments on the Google Drive PDF link. A few general comments:
I like the (new?) direction of the introduction in terms of (a) providing an exposition of what the key challenges and complexities associated with developing distributed applications are and (b) making the argument that an object model is a helpful approach to handle those complexities in appropriate ways and provide developer/user-facing simplifications which can be introspected when necessary. I think this could be even stronger with a more explicit comparison to the model of smart contracts in the EVM, covering key differences such as the object-level / TPS distinction (the EVM has no such distinction, which is one reason why common object-oriented programming paradigms don’t really work, since creating new smart contracts [EVM-objects] is very expensive), information flow control / distributed execution (the EVM does not design for this), and a focus on the essential structure of objects, messages, and transactions (the EVM includes both object-model choices and unrelated implementation details of how computation works [which in their case is actually stack/memory-based, not object-based]).
I still think that it would be helpful to spell out some details regarding what invocations are, exactly, and how object creation/destruction/lookup works, both in terms of program execution and in terms of the compilation to transaction processing systems (and correctness properties thereof). We should really be able to approach something like the “operational semantics” of a VM, with rules for how programs are interpreted.
Section 5 (on IFC) is directionally helpful, but doesn’t (yet) appear to include a concrete mathematical proposal for what IFC-labels are actually supposed to be in the AVM, and how (perhaps in the operational semantics) they will be enforced. Are you aiming to include a concrete proposal, or save that for future work? I’m relatively (perhaps naively) optimistic that we could at least provide a high-level characterization of IFC-labels/annotations in terms of object/principal identities and method invocations. Perhaps it’s all spelled out in one of the linked references, and I just need to read that? If so, it wasn’t entirely clear to me which.
Somewhat similarly, I think we can make the representation of intents in the AVM (gestured at in appendix A) much more concrete, in particular with reference to the MSC associated with a particular transaction. I think switching from a “state-oriented” perspective to a “message-oriented” one, in the context of defining intents at the object level, may be helpful. My current rough conceptual model of what this might look like is outlined here, but it certainly requires refinement – perhaps a topic to discuss.
All four points would make sense to pursue in separation. I would propose to pair 1.&3. ddapp-def-with-ifc and 2.&4. programs-n-intents
ddapp-def-with-ifc
In short, Verifiable Security Policies for Distributed Systems illustrates quite nicely for the case of secrecy what we would want to have. There are a couple of other interesting papers that have been come out recently at the intersection of logic, game theory, and model checking.