Congratulations on the formal proof and otherwise solid work. You’re almost at EAL7 with I think only one other VPN being designed as strong. Navy cancelled it, though, right before evaluation. Just add covert-channel analysis and source to object code verification to top it off. Then you’ll be Number 1 far as the implementation.
EDIT: Also, we have a formal methods tag now to highlight these posts.
It would be idea but don’t get your hopes up: big vendors usually want to use stuff like this for free or create crappy knock-offs. High-assurance security gets little love from either proprietary or FOSS sectors. It’s almost always CompSci people/companies, defense contractors, smartcard companies, or an occasional private company/person trying to create something better w/ security as differentiator. When they do, it’s uncommon for it to be FOSS (outside CompSci) since high-assurance software takes a lot of labor. They usually want something in return.
This problem led in the 1990’s to the concept of “incremental” assurance. You create a solution for the clients the fast, market-grabbing, money-making way. Make sure it’s decomposable w/ decent API or whatever to facilitate rewrites. Part of the money you make on your main product/service can be put into redoing critical parts of the software with high-assurance security. Although little data to test that, a co-founder of INFOSEC, Paul Karger, used it in his last project at IBM to fund a high-assurance, smartcard OS (Caernarvon). Broke up long-term project into intermediate deliverables IBM could sell independently and/or at least see something produced to justify funding.
Congratulations on the formal proof and otherwise solid work. You’re almost at EAL7 with I think only one other VPN being designed as strong. Navy cancelled it, though, right before evaluation. Just add covert-channel analysis and source to object code verification to top it off. Then you’ll be Number 1 far as the implementation.
EDIT: Also, we have a formal methods tag now to highlight these posts.
I guess getting the big vendors like e.g. Cisco, Check Point and Fortinet to support it will be the hardest part.
It would be idea but don’t get your hopes up: big vendors usually want to use stuff like this for free or create crappy knock-offs. High-assurance security gets little love from either proprietary or FOSS sectors. It’s almost always CompSci people/companies, defense contractors, smartcard companies, or an occasional private company/person trying to create something better w/ security as differentiator. When they do, it’s uncommon for it to be FOSS (outside CompSci) since high-assurance software takes a lot of labor. They usually want something in return.
This problem led in the 1990’s to the concept of “incremental” assurance. You create a solution for the clients the fast, market-grabbing, money-making way. Make sure it’s decomposable w/ decent API or whatever to facilitate rewrites. Part of the money you make on your main product/service can be put into redoing critical parts of the software with high-assurance security. Although little data to test that, a co-founder of INFOSEC, Paul Karger, used it in his last project at IBM to fund a high-assurance, smartcard OS (Caernarvon). Broke up long-term project into intermediate deliverables IBM could sell independently and/or at least see something produced to justify funding.
I’m not a security expert, but it’s awesome to see new (from what I read) viable alternative to VPN protocols.