This document provides security guidelines and best practices for using rules_rocq_rust in production environments, especially for security-critical applications like those in pulseengine repositories.

rules_rocq_rust is designed with security in mind, following these principles:

1. Hermetic Builds: All toolchains are downloaded and verified
2. Checksum Verification: All downloads are verified with SHA256 checksums
3. No System Dependencies: Tools are self-contained and isolated
4. Enterprise Support: Designed for air-gap and corporate environments

• Checksum Verification: All toolchain downloads are verified using SHA256 checksums
• Hermetic Downloads: Tools are downloaded from verified sources only
• No System Tools: No reliance on system-installed tools that could be compromised

• Air-Gap Support: Full offline mode with vendored toolchains
• Corporate Mirror Support: Download from internal mirrors
• Vendor Directory Support: Use shared network storage for toolchains

• Environment Variables: All sensitive configurations use environment variables
• No Hardcoded Secrets: No credentials or secrets in source code
• Minimal Permissions: Toolchain operations use least privilege

1. Verify Checksums: Always verify checksums before using toolchains
2. Use Vendored Toolchains: For production, use vendored toolchains in air-gap mode
3. Regular Updates: Keep toolchains updated with security patches
4. Monitor Dependencies: Watch for security advisories in dependencies

1. Use Verified Toolchains: Only use toolchains from trusted sources
2. Check Proof Validity: Always verify that proofs are valid and complete
3. Review Generated Code: Check coq-of-rust generated code for correctness
4. Follow Secure Coding: Apply security best practices to Rust and Coq code

1. Sign Build Artifacts: Sign all build outputs and verification results
2. Verify Before Deployment: Ensure all proofs pass before deployment
3. Monitor Build Environment: Protect build servers from tampering
4. Audit Logs: Maintain comprehensive logs of verification activities

# Enable offline mode for air-gap environments
export BAZEL_ROCQ_OFFLINE=1

# Use corporate mirror
export BAZEL_ROCQ_MIRROR=https://internal-mirror.company.com

# Use custom vendor directory
export BAZEL_ROCQ_VENDOR_DIR=/secure/vendor/toolchains

# Enable local testing (development only)
export BAZEL_ROCQ_LOCAL_TEST=1

# In MODULE.bazel - use verified toolchains
rocq = use_extension("@rules_rocq_rust//rocq:extensions.bzl", "rocq")
rocq.toolchain(
    version = "2025.01.0",
    strategy = "download",  # Hermetic download only
)

# For air-gap environments
coq_of_rust = use_extension("@rules_rocq_rust//coq_of_rust:extensions.bzl", "coq_of_rust")
coq_of_rust.toolchain(
    version = "0.5.0",
    strategy = "build",  # Build from verified source
)

• Verify all toolchain checksums
• Test toolchain downloads in staging environment
• Configure proper access controls for toolchains
• Set up monitoring for toolchain updates
• Document security procedures for your team

• Verify cryptographic algorithm implementations
• Prove security properties formally
• Test with known attack vectors
• Review proof assumptions carefully
• Document security guarantees explicitly

• Prove semantic preservation
• Verify termination properties
• Check performance guarantees
• Test edge cases thoroughly
• Document optimization invariants

# Test toolchain integrity
bazel test //test:toolchain_test

# Test download functionality
bazel test //test:real_download_test

# Test complete workflow
bazel test //test:complete_workflow_test

# Validate all proofs
bazel test //examples/advanced_validation:test_all

# Test proof metrics
bazel test //examples/advanced_validation:test_comprehensive

# Check proof coverage
bazel test //examples/advanced_validation:test_coverage

1. Isolate: Stop using potentially compromised toolchains immediately
2. Verify: Check checksums of all toolchain files
3. Replace: Use known-good toolchains from secure source
4. Investigate: Determine how compromise occurred
5. Report: Notify security team and upstream providers

1. Check Environment: Verify build environment integrity
2. Re-run Tests: Confirm failure is reproducible
3. Review Changes: Check for recent code changes
4. Isolate Issue: Determine if it's code, toolchain, or environment
5. Rollback: Use last known-good configuration if needed

• Coq Proof Engineering
• Rust Security
• Formal Methods for Security

• Bazel Security
• Supply Chain Security
• Sigstore for Verification

For security issues with rules_rocq_rust:

1. Report Privately: Contact the maintainers directly
2. Responsible Disclosure: Allow time for fixes before public disclosure
3. Provide Details: Include reproduction steps and impact assessment

Stay informed about security updates:

• Watch the GitHub repository for security advisories
• Subscribe to Coq and Rust security announcements
• Monitor formal verification toolchain security

rules_rocq_rust is licensed under Apache 2.0. This license:

• Allows free use, modification, and distribution
• Requires preservation of copyright notices
• Provides license and patent grants
• Does not impose copyleft requirements

Security Note: While the license is permissive, security is a shared responsibility. Users must ensure their specific configurations and integrations are secure.

rules_rocq_rust provides a secure foundation for formal verification, but security is a continuous process. Follow these guidelines, stay vigilant, and contribute to improving the security of the formal verification ecosystem.

Security is everyone's responsibility in the verification workflow.