In general, proofs of security for secure Multiparty Computation are based on Ideal Functionalities. For instance, see Definition 4.1 of this Simulator tutorial.
However, in a regular program in an object-oriented programming language, one deals not only with functions but with objects. Objects have functions, but also have some persistent memory.
It is possible to implement MPC objects. For instance this paper implements oblivious (i.e. MPC) arrays, dictionaries and priority queues. In these memory is persisted in a secret-shared manner which is accessed for future queries.
However, it seems that formalism for these objects is lacking. Intuitively, an MPC object should not reveal any more information than calls to some Ideal Object, which returns only (secret-shares of) the results to (secret-shared) queries on the object. Describing an Ideal Object as a sequences of calls to Ideal Functionalities does not work, because in-between the parties get correlated shares of data-structures, and so the functionalities have to be defined in reference to whatever data structure is used, rather than just in terms of the desired properties of the object.
Is there any formalism in the literature for how to prove security of MPC objects?