Repository files navigation

This project represents a flow logic analyser for the mobile ambients calculus.

[https://www2.imm.dtu.dk/GLOBAN/Nielson_1.pdf](FLOW LOGIC - Flemming Nielson & Hanne Riis Nielson)

One of the aims of the project is to perform as much analysis as possible at compile-time.

Also included is a runtime model with a rule-set based on the static analyser.

The model represents a virtual ambient machine, and hosts mobile agents that react to conditions in the process structure within the ambient simulator.

Co-algebras, typed, secure safe, and boxed, ambients are supported.I also want to model the privileges system, and the secret ambients.

We may use the join calculus to set "policies" which are basically user-definable capabilities.These setup strict rules about what can and cannot cross over ambient process boundaries.

The simulator may be launched as a service, or single-user application, and process text commands written in the ambient syntax.

Mobility and evaluation occur within a single thread, inside a given HostAmbient.Whilst capabilities is being evaluated, no mobility will occur during the synchronised phase.This is also true for processes invoked from the join table, and during all IO operations.The host ambient maintains a table of tags that represent the potential operations that may occur.Tags are randomly selected for sequential execution from the pool.The rule for process mobility is only true across ambient boundaries - a process may change it's parent, but it may notenter an ambient or leave the enclosing ambient outside of the guarded thread.

The flow tracker also uses the same tags to indicate branches in the matrix.Each tag contains a back-link to the process capability which proves thevalidity of the tag, and this is called a lemma.Finally, each tag is attached to a particular mobile-ambient.

In the runtime model, tags are evaluated in a single thread in the host ambient.Two psuedo-capabilities, enter and leave, are defined, which form the buildingblocks of all mobility operations. Boundaries between ambients are held to besynchronous - that is, mobility operations are serialised over the host-ambient.If an ambient leaves the host-ambient, it cannot be guaranteed that it willhave entered the enclosing ambient when the next operation is processed.The leave pseudo takes a single parameter, and the name of the currentenclosing ambient must match this parameter, otherwise a fault occurs.After the psudo-cap is exercised, the process will be orphaned, with aparent of null.The enter pseudo takes a single parameter, and this may be any ambient.However we test that the attached capability lemma indeed refers to achild or parent ambient, according to the rules of mobility.To enter an ambient, the process must be an orphan, ie it's parent must be null.

The Ambient hierarchy is guaranteed not to change outside the serial thread ofthe host ambient.We also have the 'exit' cap which assigns a 'leave' to every child process.A child can never 'leave' if the co-capabilities disallow it. this replaces'open' which becomes a part of the defined library capabilities, which areextensible.Co-capabilites have their own set of psuedos, which includes 'allow'and 'prevent', which can

Open caps are emulated by assigning all children of n the psuedo-cap 'leave'(via the exit psuedo-cap) causing them to exit the opened ambient.next the ambient is assigned the psuedo-cap 'leave'.

in n := leave.enter nout n := leave.enter n:parent

In the static analyser, all combinations of tags are processed, anda new permutation of the process graph is generated for each tag.any process which is restricted is excluded from the graph.

in the runtime dynamic analyser, a step-through model is used,where we evaluate each process in turn and determine which rules we apply toupdate the graph.

if a matching in cap is found, then no further in or output tags are generated.if a matching out or (bound) input is found, no further tags are generated.tags are evaluated from the top process (the host) and proceed with eachchild process, in any order. tag generation halts when an out or an inputwith a matching output are found, and the operation processed.the evaluation also halts when an in match is found, where wealready have a matching in, or if more than one output occurs; the halt occurs before tag generation - therefore,only one in match can be processed, and one output, but it may be processed alongside aneither or both an out or an input.after generation, tag processing begins. all available tags are processed, and theseare removed from their parent processes. only the pseudo-tags enter and leaveand read are processed differently, because they form the building blocks bywhich the other tags exercise the capabilities of their parent processes.

the tag processing occurs in

host ambients are not mobile themselves, although their parents might.special rules are used for boundary crossing of host ambients, and this includespi from sources external to the host. all pi and all mobility are synchonisedabout the host.

enter and leave are the only capabilities that do not result in the creation of anew software task, and are processed inline by a dedicated machine thread (per-host) ensuringthat mobility is synchronous. The pi states are also updated here, and thisincludes three operations: input, output and extrude.

extrude is a special operation.a single visible extrusion (defined by the environment) is exposed to each process.the extrude operator returns the name of a pi channel which can then be used to transmit datato the environment.and this is also done using process tags - so the process has access to the synchronousmobility feed.and this can apply to partial restricted processes too, because the type domainattached to the process, and passes through the traversal.this includes partial joins.and if the target host of the migration is an interpreter, the function can exportitself as raw source-code. otherwise, a serialised form of a reference to aparticular name is represented on a matching join in the remote host.So the output of the join compiler has to allow multiple entry points for eachfunction, as well as match against the variety of types which may be passed asinput tuples by potential users of the functions.

because the joins are processed "inline" (ie by the tag processing thread)a method invoked by the join should never block or throw.

the only time a tag may be processed by a thread other than theone attached to the tag pool is when an output occurs (from a remotehost ambient) and a matching input is waiting in the local host ambient.In this case, the input is processed by the remote ambient. Howeverit is not customary to modify the process hierarchy during an input,the hierarchy could become modified (by the host's own thread) whilstthe input join is being executed.

so to escape special conditions:if a joined method wished to perform external operations such as IOwhich may block, it should do so in a new thread not attached to thetagging layer.any operation from an IO statement should not affect the hierarchyso to perform an operation such as creating a new process, thereceiver should submit a tag for evaluation by the mobility thread.

tag creation is synchronised and may simply fail, meaning that thecreation was blocked.the pool stores a set of tags for evaluation. these are structured sothat several mobility operations may be performed in a single cycle.

tag generation starts when a host evaluation method is called.tags are created for matching capabilities and stored in the pool.if an ambient has a matching 'out' cap, a tag is generated.otherwise, it is checked for matching 'in' caps of it's siblings.

when a child ambient enters, the siblings are checked for matching 'in'caps.

when an ambient enters a new parent, it's caps are checked for amatching 'out'.

if co-caps are enabled, these form part of each check.

pi is checked before and after mobility.a waiting input with a matching output is processed first.secondly, unmatched outputs are added to the local domain.then inputs are added one by one and checked against thewaiting outputs.

These are the three main elements in a program, in the ambient functional syntax.

Domains represent areas of functional space, in which types may be defined.Each type represents a curve, or more specifically, a spline, where we specifyintersection points where domains intersect.

Domain axes are seen as terms, which are accessed using names.

We provide three types of binding.A child domain, which is subsumed by the parent.A process type, which is an applied function in the domain, so for example,the statement P|Q creates two process types, P and Q.A type constant, which is a functional pattern or rule, that can be applied toa process type. So for example, if we bind P as a constant that resolves to r,then the statement P|Q would resolve to r|Q. and this is exactly the same as saying(P|Q){P/r} .or we could bind P to a constant A[Q], in which case, P|Q resolves to A[Q]|Qwhen a process tag is evaluated, it is assumed that all the rebinding has beencompleted. however, type constants are evaluated lazily, and are representedas a simple function calls in the code. any function may be bound as a type constant.ambient names and so on are all type constants. every type constant is also anamed channel in pi. when mobility occurs, it is done through this hidden pi layer,via the implicit channel attached to the name of the mobile process.each process secretly has only one extrusion (it's own name) and this is a vectorof the names available in the runtime type domain of the process.the extrusion contains the bound names x[] and y[] which are the up and down tuplesrepresenting pi at that location. capabilities are listeners on these channels;so when an ambient moves in to a host process, the name is broadcast to thesibling processes that have matching capabilities, causing tags to be generated.the ambient has hidden processes attached, that listen for input on the localextruded channel, indicating that the ambient has a new parent. this processthen checks the local capabilites and notifies any that match, causing tagsto be generated.

the implicit names are attached to extrusions that perform the bookkeeping ofupdating the locations of each process. the bookkeeping also involves updatingthe tags attached to each ambient process. a provenance chain is created thatprovides the evidence for the location of each process. at each point in processflow, we can extrapolate the exact conditions that caused the presence of a processat a particular location.One example application for this would be an analyser which generates aprocess graph from a given piece of source-code in a particular known programminglanguage which is congruent with the compiled application.

The analysis is used to emulate the program, and discover bugs that canbe back-traced to exact locations in the source code that would be unnoticed bya standard compiler, and potentially, when coupled with an ML processor,propose changes to the source-code to make it more efficient and reliable.A back-propagating network could be trained alongside the analysis.

The type data are also expressed in meta-format, in a separate graph, so thata type environment may be queried for further information about a type-constant orprocess in it's domain.

Tags are a special kind of meta-data attached only to ambients. These are notaccessible outside the analysis simulator.

Only the type domain (and environments) are accessible to the local process.The type domain represents the entire state of the process, it's location,pi bindings, and so forth. The structures representing the process in thegraph are not exposed to the application. To perform any actions, processesutilise special pi bindings known as extrusions. Really, there is only oneextrusion - the process name - and this is used to access the processmobility layer. We can exercise capabilities, create and close child processes,and perform io, by addressing a hidden pi channel which has the name of theprocess. these operations are restricted to trusted processes.dubious processes are only permitted a pre-defined set of capabilities.special capabilities are marked with a star (asterisk), for example *enterand *leave.

We have special operators to tell us whether a name is *boundor *unbound in a domain.

And we have operators to check against grouping, *is and *not ,so that a statementin Pcan match any ambient in the group P, if the name P represents a type constantwith those operators assigned.

Join calculus is used to attach functional augmentations known as extrusions to the process tree.

Every function takes two parameters, the tuple of inputs x[] and the tuple of outputs y[].We can write these using the join syntax attached to our process as an augmentation (UDA in d-language, annotations in java, etc).Or we can have the join compiler output sourcecode to a set of files, by expanding statements in a file written in the join syntax.Standard programming languages are used for these, and the statements are mapped intoextrusions in the process graph using clauses written in a special language.These clauses deal with tuples representing names bound in pi, and also the names of thecurrent process and the parents in the hierarchy.The tuples are divided into two groups - up tuples (inputs) and down tuples (outputs).We visualise each process as a curve in the functional spectrum, with inputs above and outputs below.Parts of the function may be restricted, but we can still perform analysis on the remaining partsbecause the restricted part may be unnecessary for a particular flow check.When a function tries to read an unbound "up" tuple, or if it writes to a (really, 'the') "down" tuple before the precedingvalue has been consumed, the function yields.

A unique type domain is attached to every process, and the type domains are "parallel" at the level of theenclosing ambient.A type domain can become "restricted", which means that it has unresolved bindings, and the attached processwill be excluded from processing, but will still be included in the graph as a partial analysis.

In this way ordinary source-code can define a mixed model, by using attribute statments to attach an extrusion to any declaration in the program.

The machine provides a mechanism whereby a method or function may yield, and then become a partial function, which can migrate to another agent,possibly on a different host. We call this "ghosting".

example:P := {n = x[0] + 3y[0] = n + x[1]}

compiles to code which reads x[0] from pi, adds three to it, and binds the resultas n.the process then reads x[1] and lastly, y[0] is assigned the sum of this with the value of n.

lets say the process receives x[0] but is then migrated to a different parent.the value of n is also migrated because the local domain is attached to the process and willbe rebuild inside the remote process.

so in effect, we can switch the parent of a type domainand the bindings will reflect the migration. bindings local to the process however, will remain intact.the rebinding is done at the level of the "local ambient", meaning it's first parent in the process hierarchythat is a mobile ambient - the "enclosing ambient".

We can also write restriction policies.Lets say we have a domain alpha, and two restrictions(v n)Q(v m)(v n)Q

Q cannot exist twice in alpha, so if both n and m are bound, we have an errorbecause we have two values Q. so the restriction policy is used to supplya new value for Q that we generate to override the restriction.

Join statements

we create a join by attaching some process P to a match set.The match can contain processes and elements from local pi bindings.

eg.lets say we have a process -

P := Q[R[S]]

we can add a join to S in this location:

in P [Q.R.S in {// body of the join...}]

or we want a join with an input :

P := Q[R[S]]|

in P [Q.R.S in (^string) {// body of the join...// x[0] is bound to n}]an input at Q.R.S bound to the up tuple ^n

:= Q[R[S]]|.

in P [(^string . ^string)Q.R.S in {// body of the join...// x[0] is bound to n// x[1] is bound to m// this match will fire when two 'string' type outputs are available,// and the process S exists in both R and Q.R .// because there is only one input path, the function will never yield.}.{// body of a second join,// parallel to the first, but matching the same tuple vector.}]an input at Q.R.S bound to a string up tuple and then another one up bound to string.

P in [(^string . ^string)(^string)Q.R.* in {// body of the join...// any process in Q.R .// the match fires when a single string is available.// if any part of the join that reads the second string will be restricted// if the second string is unavailable, the join yields.// x[0] is bound to n// x[1] is bound to m}]an input at Q.R.S bound to a string up tuple and then another one up bound to string,or to simply a string bound to an up.Code which uses the second input x[1] will be automatically restricted, untilthe value is bound. the value may be seen as optional.

A yielded function is basically the same as a process waiting on a pi input capability,except that it may be waiting for more than one value, and it may be discarded, re-processedor restricted, due to changes caused by ambient mobility.

The ambient types match against statements in a defined grammar file, such as a PEG grammar.Compilation is done using the ambient flow tracking tool.After processing, the output would be the source code for the processes defined in the ambient logic.So the flow analysis helps define which output statements are used for the entities defined in the input to the compiler using the schema defined by thegrammar, and a set of rules in ambient syntax that define the behaviour of the compiler.

The compiler would be an executable program, and this would parse code according to the provided definition.Flow analysis proves that the compiled can parse any valid input, because the potential permutations of the process graph have been rendered as cases in the parser.So we know that if an error occurs in the anaylsis, the exact point in the source code can be reached by rewinding the flow graph.

The parser would send signals via a pi extrusion and these can be hooked into functions that control the output.The process has an environment which contains a set of procedures that has capabilities to open files and emit binary data.These are defined using the join syntax and standard meta-data syntax is used to apply these to the relevant statements in an ordinary programing language.

We hope to obviate the need for a separate "makefile" in our applications and have instead a global policy for each file type, that we can override using inlinemetadata in the source code.This means that the flow analyser would need to know which tools to invoke, and there would be a library of commands for each tool.

Stage one would be prototype XML and JSON etc parsers.

Eventually we would be able to specify any platform or target, and the compiler would re-analyse the entire codebase and this is done in parallel to thegenerator, so there are two process trees running.

So for any valid input, we could generate, for example:autotools "configure" and Makefile for a project.Vagrant or Docker definitions to launch pre-configured application.

We can produce any output, not necessarily an executable program, but images or sound files, or the data could be sent to a socket.The output could be an agent that migrates to a remote system.