search

cncf / tag-security

🔐CNCF Security Technical Advisory Group -- secure access, policy control, privacy, auditing, explainability and more!
https://tag-security.cncf.io
Other
2.03k stars 507 forks source link

Create cloud-native-security 2019 roadmap #146

Closed pragashj closed 3 years ago

pragashj commented 5 years ago

Create a roadmap for SAFE (cloud-native-security) cc/ @lizrice

Original SAFE roadmap document: https://github.com/cncf/sig-security/blob/master/roadmap.md

rficcaglia commented 5 years ago

I propose adding "encouraging/fostering formal specification" to the list.

ultrasaurus commented 5 years ago

@rficcaglia can you elaborate on what you mean by "formal specification?"

There are a lot of different aspects of security, policy, compliance which have been discussed, including protocols and APIs. Some parts of the landscape are fairly mature and may have formal specification elsewhere, others may benefit from a new specification, and still more may have other pre-conditions will would need to be addressed in a roadmap first.

ficcaglia commented 5 years ago

A specification using some notation that expresses behavior and/or state. Especially with respect to the security properties asserted/claimed.

Z, TLA+ are things I have used, but not advocating any particular language. one can find examples in crypto specifications (e.g. NIST publications) and other crypto publications that use mathematical notation or game models.

w8mej commented 5 years ago

Indeed. Common use cases include Amazon's Zelkova. The formal specifications are written to https://en.wikipedia.org/wiki/Satisfiability_modulo_theories .

lumjjb commented 5 years ago

I'm curious, would you consider the work of SEL4 formal specification? It uses formal methods, but doesn't define it's software based on a proof system, but instead transitively proves it.

rficcaglia commented 5 years ago

Yes absolutely i think it is a good example of a high assurance implementation

On Wed, Jul 10, 2019 at 7:13 PM Brandon Lum notifications@github.com wrote:

I'm curious, would you consider the work of SEL4 formal specification? It uses formal methods, but doesn't define it's software based on a proof system, but instead transitively proves it.

— You are receiving this because you were mentioned.

Reply to this email directly, view it on GitHub https://github.com/cncf/sig-security/issues/146?email_source=notifications&email_token=AAGENITHVAWN5J7FQHMT5ZLP62JOFA5CNFSM4HGBAVEKYY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGODZVI5RA#issuecomment-510299844, or mute the thread https://github.com/notifications/unsubscribe-auth/AAGENIWIY7CDR3PYIJFZKCTP62JOFANCNFSM4HGBAVEA .

lumjjb commented 5 years ago

I think formal methods mention is worthy in security assessments in the case where a project uses formal methods - the information would be useful in that context. Perhaps a proposal to add a section of this to the assessment outline

Formal methods is a very niche topic, so probably if it goes on the roadmap it would have to be bundled with other similar verification techniques or safeguards like using strongly typed languages or sandboxing techniques.

rficcaglia commented 5 years ago

Very few CNCF projects (any?) are using high assurance methods today...but that’s not true in other domains where formal methods are more widely used. I agree that introducing a menu of options over time, providing examples of how and where to use them, and then eventually ratcheting up the expectations is most likely to increase awareness and adoption in this particular community.

On Thu, Jul 11, 2019 at 6:14 AM Brandon Lum notifications@github.com wrote:

I think formal methods mention is worthy in security assessments in the case where a project uses formal methods - the information would be useful in that context. Perhaps a proposal to add a section of this to the assessment outline https://github.com/cncf/sig-security/blob/master/assessments/guide/outline.md

Formal methods is a very niche topic, so probably if it goes on the roadmap it would have to be bundled with other similar verification techniques or safeguards like using strongly typed languages or sandboxing techniques.

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://github.com/cncf/sig-security/issues/146?email_source=notifications&email_token=AAGENIT7G6JXQL2ALK2R4VLP64W4FA5CNFSM4HGBAVEKYY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGODZWU6JY#issuecomment-510480167, or mute the thread https://github.com/notifications/unsubscribe-auth/AAGENIWNTU6AVSX7TFLAKMTP64W4FANCNFSM4HGBAVEA .

stale[bot] commented 4 years ago

This issue has been automatically marked as inactive because it has not had recent activity.

ultrasaurus commented 3 years ago

closing cuz it is now 2021 and work will be folded into https://github.com/cncf/sig-security/issues/414