灰狐安全

2022年2月20日 (日) 03:13的版本

灰狐安全

简介

安全产品、安全咨询、安全服务

软硬件安全、可靠性、形式化验证服务是核心，OCaml（Coq） & Haskell（Agda） 是核心语言和形式化能力。

Cryptol Cryptography language，支持证明（:prove 命令）所有可能的输入的谓词（:check 命令）。

愿景

Vision：Building a comprehensive open source security platform.

路线图

DevSecOps + AISecOps 共筑下一代安全体系

1、DevSecOps 将安全置于 DevOps 整个生命周期 DevSecOps is a combination of Compliance Operations, Security Engineering, Security Science, and Security Operations.

2、AISecOps 人工智能自动化云安全服务 AISecOps as a holistic cloud operations and security management framework that covers the full-stack and incorporates AI to deliver automated response and incident management.

3、通过 PostgreSQL/Greenplum 建立分布式数据仓库 集中数据存储 机器学习和深度学习下沉至数据库 数据库内建机器学习和人工智能算法：一切皆 SQL

商业模式：安全服务具有连续性、持续性，企业每年都要交纳的服务费。

应用场景：如：基于日志的入侵检测分析、利用MADlib图算法检测异常行为

技术融合，交付更大价值的安全服务。

OpenSSF

跟进 Open Source Security Foundation (OpenSSF) 尤其 Security Scorecards 项目。

DevSecOps

DevSecOps 通过自动检测和修复漏洞并免受目标性攻击和自动攻击程序的影响，

无需扫描或者调度，让软件能够自我防护。就像给你的应用程序打了疫苗。

应用场景：

• 自动进行渗透测试以优化资源
• 安全团队与敏捷（Agile） & 开发运营（DevOps）保持同步
• 安全即规范，开发速度更快、构建更安全、无时无刻的监测
• 攻击监测 = 应用安全监测（ASM）持续的可见性、应用智能、迅速响应
• 云安全，安全可扩展
• 帮助企业满足特定的安全合规性标准

OSINT

Open Source Intelligence (OSINT) 开源情报

Haskell

Galois Trust your most critical systems, Galois’s open source verification tools (SAW Cryptol and Crux).

Cryptol Cryptography language, Ivory EDSL, Software Analysis Workbench (SAW) 带来全新的安全思维。

OCaml

静态分析、代码质量、代码安全

Infer in the "static analysis world", OCaml is one of the most popular languages.

ocaml-tls TLS in pure OCaml.

Identity

Open Source Identity and Access Management

• ORY The new identity platform
• 狗狗通行证

区块链

区块链和数字货币安全

区块链和智能合约的 Formal verification

操作系统

• OPNsense & pfSense Firewall, VPN, and Router
• Linux grsecurity 安全补丁集
• HardenedBSD 主要目标是 grsecurity 的重新实现, GitLab 仓库
• FreeBSD + LLVM

数据库存储

• ZFS
• FreeBSD Enterprise Storage
• Serving Netflix Video at 400Gb/s on FreeBSD

项目

• Open Policy Agent
• Vault
• Wazuh 基于趋势科技的 OSSEC 构建（分支），Migrating from OSSEC
• PKI, CA, TLS, GnuTLS
• LDAP, Apache Directory, OpenLDAP
• lego Let's Encrypt client and ACME library written in Go.
• StackStorm
• falco

形式化验证

我们核心关注软件和硬件的完全功能正确性的规范和验证。

DeepSpec 是一个有关软硬件规范（软件应该做什么）和形式化验证的技术联盟，主要专注核心系统软件，如：操作系统、编程语言编译器和计算机芯片等。

我们关注的形式化验证/证明助手语言有：OCaml 编写的 Coq、Haskell 编写的 Agda、Common Lisp 编写的 ACL2。

HACL* a formally verified cryptographic library（形式化验证密码学库）written in F*

Solidity Formally Verified Smart Contracts

服务

• Formal Verification（形式化验证） for Blockchain & Smart Contracts and Software & Hardware
• Zero Trust Architecture（零信任架构）
• Security Analytics（安全分析）
• Intrusion Detection（入侵检测）
• Log Data Analysis（日志数据分析）
• File Integrity Monitoring（文件完整性监控）
• Vulnerability Detection（漏洞检测）
• Configuration Assessment（配置评估）
• Incident Response（应急响应）
• Regulatory Compliance（合规性）
• Cloud Security Monitoring（云安全监控）
• Container Security（容器安全）
• Database Security（数据库安全）
• Mobile Security（移动安全）

运营支撑

Haskell + PostgREST + PostgreSQL 是整个产品和技术体系的软件基础设施。

图集

• 

  云访问安全代理(CASB)

• 

  Wazuh

• 

  Wazuh数据流

• 

  Wazuh Agent

• 

  Wazuh Server

• 

  Wazuh部署

• 

  Cryptol REPL

链接

• Runtime Verification Inc We love formal methods
• OWASP
• Awesome Hacking
• Contrast
• Sonatype Automate DevSecOps
• 网络安全类公众号推荐
• Azure Key Vault