1use std::collections::{BTreeMap, BTreeSet};
50use std::sync::Arc;
51
52use beck_diag::{Diagnostic, Diagnostics, Span};
53
54use crate::check::Program;
55use crate::core::{CoreKind, Prim};
56use crate::ty::{Effect, Tier, Ty, TyDecl};
57
58#[derive(Clone, Debug, PartialEq, Eq)]
60pub struct NotSendable {
61 pub offender: String,
63 pub path: Vec<String>,
65 pub why: &'static str,
66}
67
68impl NotSendable {
69 pub fn flow(&self) -> String {
70 self.path.join(".")
71 }
72}
73
74pub fn sendable(ty: &Ty, types: &BTreeMap<Arc<str>, TyDecl>) -> Result<(), NotSendable> {
77 check(ty, types, Rule::Sendable)
78}
79
80pub fn storable(ty: &Ty, types: &BTreeMap<Arc<str>, TyDecl>) -> Result<(), NotSendable> {
88 check(ty, types, Rule::Storable)
89}
90
91#[derive(Clone, Copy, PartialEq, Eq)]
92enum Rule {
93 Sendable,
94 Storable,
95}
96
97fn check(ty: &Ty, types: &BTreeMap<Arc<str>, TyDecl>, rule: Rule) -> Result<(), NotSendable> {
98 fn go(
99 ty: &Ty,
100 types: &BTreeMap<Arc<str>, TyDecl>,
101 rule: Rule,
102 path: &mut Vec<String>,
103 seen: &mut BTreeSet<Arc<str>>,
104 ) -> Result<(), NotSendable> {
105 let fail = |offender: String, why: &'static str, path: &Vec<String>| {
106 Err(NotSendable {
107 offender,
108 path: path.clone(),
109 why,
110 })
111 };
112 match ty {
113 Ty::Var(_) => Ok(()),
114 Ty::Fun(..) => fail(
115 format!("{ty}"),
116 "a function is code, and code does not cross a boundary as data",
117 path,
118 ),
119 Ty::Con(name, args) => {
120 match name.as_ref() {
121 Ty::SECRET => {
122 return fail(
123 format!("{ty}"),
124 "`secret[T]` is deliberately not Sendable: that is the whole mechanism",
125 path,
126 )
127 }
128 Ty::INTERNAL if rule == Rule::Sendable => {
131 return fail(
132 format!("{ty}"),
133 "`internal[T]` is recorded and never shown: it may be written to the \
134 log and may not cross a boundary",
135 path,
136 )
137 }
138 Ty::HTML | Ty::ATTR if rule == Rule::Storable => {
139 return fail(
140 format!("{ty}"),
141 "a view is derived from state, so storing one would make replay read \
142 it back rather than recompute it",
143 path,
144 )
145 }
146 _ => {}
147 }
148 for (i, a) in args.iter().enumerate() {
149 path.push(format!("[{i}]"));
150 go(a, types, rule, path, seen)?;
151 path.pop();
152 }
153 let Some(decl) = types.get(name.as_ref()) else {
154 return Ok(());
155 };
156 if !seen.insert(name.clone()) {
157 return Ok(());
159 }
160 let out = match decl {
161 TyDecl::Model { fields, .. } => {
162 for (f, t) in fields {
163 path.push(f.to_string());
164 go(t, types, rule, path, seen)?;
165 path.pop();
166 }
167 Ok(())
168 }
169 TyDecl::Union { variants, .. } => {
170 for v in variants {
171 for (f, t) in &v.fields {
172 path.push(format!("{}.{f}", v.name));
173 go(t, types, rule, path, seen)?;
174 path.pop();
175 }
176 }
177 Ok(())
178 }
179 TyDecl::Newtype { inner, .. } | TyDecl::Alias { ty: inner, .. } => {
180 go(inner, types, rule, path, seen)
181 }
182 };
183 seen.remove(name.as_ref());
184 out
185 }
186 }
187 }
188 let mut path = vec![format!("{ty}")];
189 let mut seen = BTreeSet::new();
190 go(ty, types, rule, &mut path, &mut seen)
191}
192
193#[derive(Clone, Debug)]
195pub struct Reach {
196 pub what: Arc<str>,
197 pub tier: Tier,
198 pub blocked: Option<&'static str>,
199}
200
201pub fn flow(program: &Program, ty_name: &str) -> Vec<Reach> {
204 let mut out = Vec::new();
205 for name in &program.def_order {
206 let Some(d) = program.defs.get(name) else {
207 continue;
208 };
209 let mentions = std::iter::once(&d.ret)
210 .chain(d.params.iter().map(|(_, _, t)| t))
211 .any(|t| mentions_type(t, ty_name, &program.types));
212 if !mentions {
213 continue;
214 }
215 out.push(Reach {
216 what: d.name.clone(),
217 tier: d.tier,
218 blocked: (d.tier == Tier::Client).then_some("a client cannot hold a `secret[T]`"),
219 });
220 }
221 for s in &program.signals {
222 if !mentions_type(&s.ty, ty_name, &program.types) {
223 continue;
224 }
225 out.push(Reach {
226 what: s.name.clone(),
227 tier: s.tier,
228 blocked: (s.tier == Tier::Client).then_some("a client cannot hold a `secret[T]`"),
229 });
230 }
231 out
232}
233
234pub fn flow_report(program: &Program, ty_name: &str) -> Result<String, String> {
239 use std::fmt::Write;
240 let Some(decl) = program.types.get(ty_name) else {
241 return Err(format!("no type `{ty_name}` in this program"));
242 };
243 let is_secret = sendable(&Ty::con(ty_name), &program.types).err();
244 let mut out = String::new();
245 let _ = writeln!(
246 out,
247 "{ty_name} ({}) — {}",
248 match decl {
249 TyDecl::Model { .. } => "model",
250 TyDecl::Union { .. } => "union",
251 TyDecl::Newtype { .. } => "newtype",
252 TyDecl::Alias { .. } => "alias",
253 },
254 match &is_secret {
255 Some(bad) => format!("not Sendable: {} at {}", bad.offender, bad.flow()),
256 None => "Sendable".to_string(),
257 }
258 );
259
260 let reached = flow(program, ty_name);
261 if reached.is_empty() {
262 let _ = writeln!(out, "\n reaches nothing — no signature mentions it");
263 return Ok(out);
264 }
265 let _ = writeln!(out);
266 for r in &reached {
267 match (&r.blocked, &is_secret) {
268 (Some(why), Some(_)) => {
269 let _ = writeln!(out, " BLOCKED: {:<18} {:<8} {why}", r.what, r.tier.name());
270 }
271 _ => {
272 let _ = writeln!(out, " reaches: {:<18} {:<8} ok", r.what, r.tier.name());
273 }
274 }
275 }
276 if is_secret.is_some() {
277 let _ = writeln!(
278 out,
279 "\na crossing requires Sendable, and `secret[T]` is deliberately not \
280 (docs/03 §3.5).\nWhat blocks the leak is the placement, so moving one of \
281 these to the client is the compile error."
282 );
283 }
284 Ok(out)
285}
286
287fn mentions_type(ty: &Ty, name: &str, types: &BTreeMap<Arc<str>, TyDecl>) -> bool {
288 fn go(
289 ty: &Ty,
290 name: &str,
291 types: &BTreeMap<Arc<str>, TyDecl>,
292 seen: &mut BTreeSet<Arc<str>>,
293 ) -> bool {
294 match ty {
295 Ty::Var(_) => false,
296 Ty::Fun(ps, r, _) => {
297 ps.iter().any(|p| go(p, name, types, seen)) || go(r, name, types, seen)
298 }
299 Ty::Con(n, args) => {
300 if n.as_ref() == name {
301 return true;
302 }
303 if args.iter().any(|a| go(a, name, types, seen)) {
304 return true;
305 }
306 if !seen.insert(n.clone()) {
307 return false;
308 }
309 match types.get(n.as_ref()) {
310 Some(TyDecl::Model { fields, .. }) => {
311 fields.iter().any(|(_, t)| go(t, name, types, seen))
312 }
313 Some(TyDecl::Union { variants, .. }) => variants
314 .iter()
315 .any(|v| v.fields.iter().any(|(_, t)| go(t, name, types, seen))),
316 Some(TyDecl::Newtype { inner, .. }) | Some(TyDecl::Alias { ty: inner, .. }) => {
317 go(inner, name, types, seen)
318 }
319 None => false,
320 }
321 }
322 }
323 }
324 go(ty, name, types, &mut BTreeSet::new())
325}
326
327pub fn check_security(program: &Program, diags: &mut Diagnostics) {
343 check_boundaries(program, diags);
344 check_capabilities(program, diags);
345}
346
347pub fn check_boundaries(program: &Program, diags: &mut Diagnostics) {
349 boundaries(program, diags);
350}
351
352pub fn check_capabilities(program: &Program, diags: &mut Diagnostics) {
354 capabilities(program, diags);
355}
356
357fn boundaries(program: &Program, diags: &mut Diagnostics) {
359 for s in &program.signals {
360 if s.effects.contains(&Effect::Durable) {
362 let state = element(&s.ty);
363 if let Err(bad) = storable(&state, &program.types) {
364 reject(
365 diags,
366 "B0411",
367 format!("`{}` is durable, so its state must be storable", s.name),
368 s.span,
369 &bad,
370 "the log is the only description of this program's history; a value it cannot \
371 read back is a state replay would not reproduce",
372 );
373 }
374 }
375 if s.tier == Tier::Client {
377 let carried = element(&s.ty);
378 if let Err(bad) = sendable(&carried, &program.types) {
379 reject(
380 diags,
381 "B0410",
382 format!(
383 "`{}` runs on the client, so its value must be Sendable",
384 s.name
385 ),
386 s.span,
387 &bad,
388 "this value crosses to the browser; §3.5's whole claim is that the compiler \
389 proves it cannot carry a secret",
390 );
391 }
392 }
393 }
394
395 if let Some(TyDecl::Union { .. }) = program.types.get("Command") {
397 if let Err(bad) = sendable(&Ty::con("Command"), &program.types) {
398 let span = program
399 .signals
400 .first()
401 .map(|s| s.span)
402 .unwrap_or(Span::NONE);
403 reject(
404 diags,
405 "B0410",
406 "`Command` is what clients send, so it must be Sendable".to_string(),
407 span,
408 &bad,
409 "a command is minted in the browser: a secret in one would be a secret the browser \
410 already had",
411 );
412 }
413 }
414
415 for name in &program.def_order {
417 let Some(d) = program.defs.get(name) else {
418 continue;
419 };
420 if d.tier != Tier::Client {
421 continue;
422 }
423 for t in std::iter::once(&d.ret).chain(d.params.iter().map(|(_, _, t)| t)) {
424 if let Err(bad) = sendable(t, &program.types) {
425 let kind = if bad.offender.starts_with("secret[") {
429 "a secret"
430 } else if bad.offender.starts_with("internal[") {
431 "an internal fact"
432 } else {
433 continue;
434 };
435 reject(
436 diags,
437 "B0410",
438 format!("`{}` runs on the client and handles {kind}", d.name),
439 d.span,
440 &bad,
441 "`beck explain flow` shows the whole path; the fix is to keep the \
442 definition on a tier that can hold it",
443 );
444 }
445 }
446 }
447}
448
449fn reject(
450 diags: &mut Diagnostics,
451 code: &'static str,
452 message: String,
453 span: Span,
454 bad: &NotSendable,
455 note: &str,
456) {
457 diags.push(
458 Diagnostic::error(code, message, span)
459 .with_primary_label(format!("`{}` reaches it at `{}`", bad.offender, bad.flow()))
460 .with_note(bad.why)
461 .with_note(note.to_string()),
462 );
463}
464
465fn element(t: &Ty) -> Ty {
466 match t {
467 Ty::Con(n, args)
468 if (n.as_ref() == Ty::SIGNAL || n.as_ref() == Ty::STREAM) && args.len() == 1 =>
469 {
470 args[0].clone()
471 }
472 other => other.clone(),
473 }
474}
475
476fn capabilities(program: &Program, diags: &mut Diagnostics) {
485 if !has_chokepoint(program) {
489 return;
490 }
491 let authorised = reachable_from_validator(program);
492 for name in &program.def_order {
493 let Some(d) = program.defs.get(name) else {
494 continue;
495 };
496 let caps: Vec<&Effect> = d
497 .effects
498 .iter()
499 .filter(|e| matches!(e, Effect::Cap(_)))
500 .collect();
501 if caps.is_empty() || authorised.contains(name) {
502 continue;
503 }
504 let names: Vec<String> = caps.iter().map(|e| e.name()).collect();
505 diags.push(
506 Diagnostic::error(
507 "B0412",
508 format!("`{name}` requires a capability nothing can discharge"),
509 d.span,
510 )
511 .with_primary_label(format!("needs {{{}}}", names.join(", ")))
512 .with_note(
513 "a `Session` reaches exactly one place in a Beck program: the validator `decide` is \
514 given, which is the only function handed a `Proposal`. Authority is one chokepoint \
515 (docs/03 §3.5), so a capability required outside it has no holder",
516 )
517 .with_fix(
518 "call this from `validate` — or, if it genuinely needs no authority, drop the \
519 `cap.*` from its `uses`",
520 ),
521 );
522 }
523}
524
525fn has_chokepoint(program: &Program) -> bool {
527 program.signals.iter().any(|s| {
528 matches!(
529 &s.expr.kind,
530 CoreKind::Prim {
531 op: Prim::Decide,
532 ..
533 }
534 )
535 })
536}
537
538fn reachable_from_validator(program: &Program) -> BTreeSet<Arc<str>> {
540 let mut roots: Vec<Arc<str>> = Vec::new();
541 for s in &program.signals {
542 if let CoreKind::Prim {
543 op: Prim::Decide,
544 args,
545 } = &s.expr.kind
546 {
547 if let Some(v) = args.get(2) {
548 let mut names = BTreeSet::new();
549 crate::place::mentions(v, &mut names);
550 roots.extend(names);
551 }
552 }
553 }
554 let mut out: BTreeSet<Arc<str>> = BTreeSet::new();
555 while let Some(n) = roots.pop() {
556 if !out.insert(n.clone()) {
557 continue;
558 }
559 if let Some(d) = program.defs.get(&n) {
560 let mut names = BTreeSet::new();
561 crate::place::mentions(&d.body, &mut names);
562 roots.extend(names);
563 }
564 }
565 out
566}
567
568#[cfg(test)]
569mod tests {
570 use super::*;
571 use crate::{check_str, compile_str};
572
573 fn types() -> BTreeMap<Arc<str>, TyDecl> {
574 BTreeMap::from([
575 (
576 Arc::from("Config"),
577 TyDecl::Model {
578 name: Arc::from("Config"),
579 params: Vec::new(),
580 fields: vec![
581 (Arc::from("host"), Ty::str_()),
582 (Arc::from("key"), Ty::secret(Ty::str_())),
583 ],
584 },
585 ),
586 (
587 Arc::from("State"),
588 TyDecl::Model {
589 name: Arc::from("State"),
590 params: Vec::new(),
591 fields: vec![(Arc::from("config"), Ty::con("Config"))],
592 },
593 ),
594 ])
595 }
596
597 #[test]
598 fn a_secret_is_not_sendable_however_deeply_it_is_buried() {
599 let t = types();
600 assert!(sendable(&Ty::str_(), &t).is_ok());
601 let bad = sendable(&Ty::con("State"), &t).expect_err("State reaches a secret");
602 assert_eq!(bad.flow(), "State.config.key");
604 assert_eq!(bad.offender, "secret[Str]");
605 assert!(sendable(&Ty::list(Ty::con("Config")), &t).is_err());
607 assert!(sendable(&Ty::map(Ty::str_(), Ty::con("Config")), &t).is_err());
608 }
609
610 #[test]
611 fn a_view_may_cross_a_boundary_but_may_not_be_stored() {
612 let t = types();
616 assert!(sendable(&Ty::html(), &t).is_ok());
617 assert!(storable(&Ty::html(), &t).is_err());
618 }
619
620 #[test]
621 fn a_recursive_type_terminates() {
622 let t = BTreeMap::from([(
623 Arc::from("Tree"),
624 TyDecl::Model {
625 name: Arc::from("Tree"),
626 params: Vec::new(),
627 fields: vec![(Arc::from("kids"), Ty::list(Ty::con("Tree")))],
628 },
629 )]);
630 assert!(sendable(&Ty::con("Tree"), &t).is_ok());
631 }
632
633 #[test]
634 fn a_state_that_caches_a_view_is_refused_at_compile_time() {
635 let src = crate::split::tests::TODO.replace(
639 "model State:\n todos: Map[Id, Todo]",
640 "model State:\n todos: Map[Id, Todo]\n cached: Html",
641 );
642 let (_, d, _) = compile_str("t.beck", &src);
643 let codes: Vec<&str> = d.iter().map(|x| x.code).collect();
644 assert!(codes.contains(&"B0411"), "got {codes:?}");
645 }
646
647 #[test]
648 fn a_secret_in_the_command_union_is_refused() {
649 let src = crate::split::tests::TODO.replace(
652 "union Command:\n Add(id: Id, text: Str)",
653 "union Command:\n Add(id: Id, text: Str, token: secret[Str])",
654 );
655 let (_, d, _) = compile_str("t.beck", &src);
656 let codes: Vec<&str> = d.iter().map(|x| x.code).collect();
657 assert!(codes.contains(&"B0410"), "got {codes:?}");
658 }
659
660 #[test]
661 fn a_capability_required_outside_the_chokepoint_has_no_holder() {
662 let src = crate::split::tests::TODO.replace(
663 "def done_class(t: Todo) -> Str:",
664 "def audit(t: Todo) -> Str uses cap.admin:\n return t.text\n\n\
665 def done_class(t: Todo) -> Str:",
666 );
667 let (_, d, _) = compile_str("t.beck", &src);
668 let codes: Vec<&str> = d.iter().map(|x| x.code).collect();
669 assert!(codes.contains(&"B0412"), "got {codes:?}");
670 }
671
672 #[test]
673 fn a_capability_required_inside_the_chokepoint_is_exactly_what_it_is_for() {
674 let src = crate::split::tests::TODO
677 .replace(
678 "def owned(s: State, p: Proposal, id: Id, evs: list[Event])",
679 "def admin(p: Proposal) -> Bool uses cap.admin:\n\
680 \x20 return p.session.actor != \"\"\n\n\
681 def owned(s: State, p: Proposal, id: Id, evs: list[Event])",
682 )
683 .replace(
684 " match map_get(s.todos, id):\n case Some(value):\n if value.owner != p.session.actor:",
685 " match map_get(s.todos, id):\n case Some(value):\n if not admin(p):",
686 );
687 let (program, d, map) = check_str("t.beck", &src);
688 assert!(!d.has_errors(), "{}", d.render(&map));
689 let mut diags = Diagnostics::new();
690 let solution = crate::place::solve(&program, None);
691 let mut program = program;
692 crate::place::apply(&mut program, &solution);
693 check_security(&program, &mut diags);
694 assert!(
695 !diags.iter().any(|x| x.code == "B0412"),
696 "{}",
697 diags.render(&map)
698 );
699 assert_eq!(
700 program.defs["admin"].tier,
701 Tier::Server,
702 "only the server holds a capability"
703 );
704 }
705
706 #[test]
707 fn explain_flow_names_the_definitions_a_type_reaches() {
708 let src = "\
709model Config:
710 key: secret[Str]
711
712def load() -> Config uses env:
713 return Config(key=secret_env(\"API_KEY\"))
714
715def host(c: Config) -> Str:
716 return \"api.example.com\"
717";
718 let (program, d, map) = check_str("t.beck", src);
719 assert!(!d.has_errors(), "{}", d.render(&map));
720 let reached: Vec<String> = flow(&program, "Config")
721 .into_iter()
722 .map(|r| r.what.to_string())
723 .collect();
724 assert_eq!(reached, ["load", "host"]);
725 }
726}
727
728#[cfg(test)]
729mod quadrants {
730 use super::*;
731
732 #[test]
735 fn the_two_axes_are_independent() {
736 let types: BTreeMap<Arc<str>, TyDecl> = BTreeMap::new();
737 let quad = |t: &Ty| (sendable(t, &types).is_ok(), storable(t, &types).is_ok());
738
739 assert_eq!(quad(&Ty::str_()), (true, true), "ordinary data does both");
740 assert_eq!(
741 quad(&Ty::html()),
742 (true, false),
743 "a view crosses as patches and is never read back from the log"
744 );
745 assert_eq!(
746 quad(&Ty::internal(Ty::str_())),
747 (false, true),
748 "`internal[T]` is the quadrant `secret[T]` alone left empty"
749 );
750 assert_eq!(
751 quad(&Ty::secret(Ty::str_())),
752 (false, false),
753 "a token reaches neither the browser nor the log (§3.7 F5)"
754 );
755 assert_eq!(
756 quad(&Ty::fun(vec![Ty::int()], Ty::int())),
757 (false, false),
758 "code is not data in either direction"
759 );
760 }
761
762 #[test]
763 fn an_internal_field_is_found_however_deeply_it_is_buried() {
764 let types = BTreeMap::from([(
765 Arc::from("Suspension"),
766 TyDecl::Model {
767 name: Arc::from("Suspension"),
768 params: Vec::new(),
769 fields: vec![
770 (Arc::from("at"), Ty::int()),
771 (Arc::from("reason"), Ty::internal(Ty::str_())),
772 ],
773 },
774 )]);
775 let bad = sendable(&Ty::list(Ty::con("Suspension")), &types)
776 .expect_err("a list of them still cannot cross");
777 assert_eq!(bad.flow(), "list[Suspension].[0].reason");
778 assert!(storable(&Ty::list(Ty::con("Suspension")), &types).is_ok());
780 }
781}