This has been done a few times, one recent example is Quark: http://goto.ucsd.edu/quark/
On 07/11/2014 01:02 PM, Sven Kieske wrote: > On 11.07.2014 17:58, Matt DeMoss wrote: >> For legacy code, what about sandboxing it and then proving >> something about the sandbox? Not sure if that's really in the >> spirit of verification you had in mind. > Well if your sandbox would be proven to be secure there is still > the problem: How does the legacy code behave inside the sandbox? Is > it acceptable that it maybe just breaks when the sandbox refuses to > do $x ? So to my understanding you must not just prove the sandbox > itself, rather show that the interaction between sandbox and legacy > code are "ok". > > Without going into details or a specific example I still got the > feeling this could be more complex than just proving the legacy > code/rewrite that code. > > kind regards > > Sven _______________________________________________ > langsec-discuss mailing list langsec-discuss@mail.langsec.org > https://mail.langsec.org/cgi-bin/mailman/listinfo/langsec-discuss > _______________________________________________ langsec-discuss mailing list langsec-discuss@mail.langsec.org https://mail.langsec.org/cgi-bin/mailman/listinfo/langsec-discuss
