<p>As it turns out, there is some fascinating work done in this direction. </p>

<p>In particular, in 2003, Michael Howard, Jon Pincus, and Jeannette M. Wing's <em>Measuring Relative Attack Surfaces</em> in proceedings of Workshop on Advanced Developments in Software and Systems Security, Taipei, December 2003.  </p>

<p>Further work by the same authors over the years is quite interesting ... For anyone who found my question of interest you can check their work out at <a href="http://www.cs.cmu.edu/~pratyus/as.html" rel="nofollow">http://www.cs.cmu.edu/~pratyus/as.html</a> ... And if you find them interesting, i hope that you will find my work interesting too :)</p>

CC BY-SA 3.0
2011-12-24T11:06:18.347Z
2011-12-24T11:06:18.347Z
Ahmed Masud
<p>I think that software model checking, in the vein of <a href="http://alloy.mit.edu/alloy/" rel="nofollow">Alloy</a>, is probably related to what you're looking for.  You write a model, and also a specification that the model should satisfy, and check if they're related appropriately. </p>

CC BY-SA 3.0
2011-12-15T01:33:37.103Z
Alloy is a very interesting suggestion :)
Ahmed Masud
CC BY-SA 3.0
2011-12-14T15:22:24.197Z
2011-12-14T15:22:24.197Z
Sam Tobin-Hochstadt
<p>I am attempting to develop some notions of a difference-calculus between a notional Ideal Turing Machine conceived by a developer (e.g. whatever is intended by a software developer), call it $M_I$, and the Machines that represent the software which actually gets designed and implemented, say $M_\alpha$ and $M_\beta$, respectively. </p>

<p>Specifically, my interest is in examining limitations (due to Rice's Theorem for instance) in automated detection of errors in software programs between the Language processed by the ideal machine, and the language processed by the developed/implemented Machines.</p>

<p>Any reference to prior work that works with some notions of exploring differences between two specified Turing Machines, or barring that a lower level Formal Language would be extremely helpful and appreciated; because i'd rather cite than write :-).</p>

CC BY-SA 3.0
2011-12-14T07:24:17.047Z
Sounds like [model-based testing](http://en.wikipedia.org/wiki/Model-based_testing). One develops a model of the desired system and then uses this to generate tests for the actual system.
Dave Clarke
CC BY-SA 3.0
2011-12-14T09:35:18.237Z
@DaveClarke thank you for the cross-reference to model-based testing, it should've occurred to me there are definite benefits to looking at model-based testing ... i wonder if i start with just FSA and build up i may be able to utilize a lot of the existing theory on fault modelling. (just thinking out loud)
Ahmed Masud
CC BY-SA 3.0
2011-12-14T14:57:02.763Z
I'd also look at the theories of program refinement and the refinement calculus. R.-J. Back and J. von Wright have developed this theory. In the world of concurrent programming, there is the related concept of action refinement.
Martin Berger
CC BY-SA 3.0
2011-12-16T15:16:17.127Z
@MartinBerger thank you for the suggestion of looking into action refinement.  Specifically Action Refinement in Process Algebra and Security Issues http://www.dsi.unive.it/~srossi/Papers/lopstr07.pdf was an interesting find for sure!
Ahmed Masud
CC BY-SA 3.0
2011-12-16T15:21:47.320Z
General update: The technical report "Attack Modeling for Information Security and Survivability" by Moore, A.P. and Ellison, R.J. and Linger, R.C.; provides a good starting basis.

P.S. I may end up posting an answer to my own question as derived by all the wonderful suggestions by everyone.. Is that usual?
Ahmed Masud
<lo.logic><computability><pl.programming-languages><model-checking><program-verification>
Is there any work done on developing difference-calculus of Turing Machines (or simpler Formal Languages)
Ahmed Masud
# Is there any work done on developing difference-calculus of Turing Machines (or simpler Formal Languages)

(Asked by: username_0 on 2011-12-14)

I am attempting to develop some notions of a difference-calculus between a notional Ideal Turing Machine conceived by a developer (e.g. whatever is intended by a software developer), call it $M\_I$, and the Machines that represent the software which actually gets designed and implemented, say $M\_\alpha$ and $M\_\beta$, respectively.

Specifically, my interest is in examining limitations (due to Rice's Theorem for instance) in automated detection of errors in software programs between the Language processed by the ideal machine, and the language processed by the developed/implemented Machines.

Any reference to prior work that works with some notions of exploring differences between two specified Turing Machines, or barring that a lower level Formal Language would be extremely helpful and appreciated; because i'd rather cite than write :-).

**Tags:** lo.logic, computability, pl.programming-languages, model-checking, program-verification
> **Comments:**
> **username_1**: Sounds like [model-based testing](http://en.wikipedia.org/wiki/Model-based_testing). One develops a model of the desired system and then uses this to generate tests for the actual system.  
> **username_0**: @DaveClarke thank you for the cross-reference to model-based testing, it should've occurred to me there are definite benefits to looking at model-based testing ... i wonder if i start with just FSA and build up i may be able to utilize a lot of the existing theory on fault modelling. (just thinking out loud)  
> **username_2**: I'd also look at the theories of program refinement and the refinement calculus. R.-J. Back and J. von Wright have developed this theory. In the world of concurrent programming, there is the related concept of action refinement.  
> **username_0**: @MartinBerger thank you for the suggestion of looking into action refinement.  Specifically Action Refinement in Process Algebra and Security Issues http://www.dsi.unive.it/~srossi/Papers/lopstr07.pdf was an interesting find for sure!  
> **username_0**: General update: The technical report "Attack Modeling for Information Security and Survivability" by Moore, A.P. and Ellison, R.J. and Linger, R.C.; provides a good starting basis.  P.S. I may end up posting an answer to my own question as derived by all the wonderful suggestions by everyone.. Is that usual?  

---

## 2 answers

### Answer by username_0 on 2011-12-24. Score: 3 | Accepted answer

As it turns out, there is some fascinating work done in this direction.

In particular, in 2003, Michael Howard, Jon Pincus, and Jeannette M. Wing's *Measuring Relative Attack Surfaces* in proceedings of Workshop on Advanced Developments in Software and Systems Security, Taipei, December 2003.

Further work by the same authors over the years is quite interesting ... For anyone who found my question of interest you can check their work out at <http://www.cs.cmu.edu/~pratyus/as.html> ... And if you find them interesting, i hope that you will find my work interesting too :)


---

### Answer by username_3 on 2011-12-14. Score: 2

I think that software model checking, in the vein of [Alloy](http://alloy.mit.edu/alloy/), is probably related to what you're looking for. You write a model, and also a specification that the model should satisfy, and check if they're related appropriately.

> **Comments:**
> **username_0**: Alloy is a very interesting suggestion :)  

---

