Towards SOS meta-theory for language-based security

SOS meta-theory has been very successful in defining meta-theorems using which one can prove useful properties about language constructs. These meta-theorems can save pages of standard proof thanks to their generic and language-independent formulation. Security properties of language constructs look like promising candidates to be turned into SOS meta-theorems and there has already been an attempt in this direction in the context of process calculi security. In this paper, we give an exploratory account of this issue in the context of language-based security. To do this, we give a superficial overview of information-flow security and in particular, non-interference as a central notion in this field. Then, we point out some interesting links between non-interference and our recent work on notions of bisimulation with data. Finally, some ideas regarding SOS meta-theorems for these notions are presented.