@Alex Crichton @fitzgen (he/him) @Jonathan Foote this bug, which was created right after the oss-fuzz integration was set up, and seems to be some kind of problem with the setup, says that it'd be closed within a day after being fixed—does that mean it's not fixed yet? https://bugs.chromium.org/p/oss-fuzz/issues/detail?id=20472&q=label%3AProj-wasmtime
I think that this is trying to build with clang coverage, which is not supported by rustc.
Looking at the build logs I see stuff like:
Step #5: du: cannot access '/workspace/out/coverage/dumps/compile.*.profraw': No such file or directory Step #5: du: cannot access '/workspace/out/coverage/dumps/instantiate.*.profraw': No such file or directory
oh I forgot about that...
I opened up https://github.com/google/oss-fuzz/issues/3468
"fixed" :D
heh, yes, "fixed". Thank you for handling this!
Hello all. Apologies for the delay in responding here, I was OOO last week :electric_plug: For context, I asked Max (Dor1s) and a few other people about the possibility of google providing resources to work on this when I saw him IRL two weeks ago. Unfortunately it sounds like they probably won't, at least from his perspective.
IIUC we would effectively want https://github.com/rust-lang/rust/issues/34701 addressed
I will mention it on the relevant oss-fuzz GH issue
This would be nice to have for sure when evaluating whether a fuzz target is exercising all the corners you expect it to. AFAIK, we "just" need to do the work in rustc
to hook this stuff up. @Alex Crichton would know more. Not sure how to prioritize working on this vs other wasmtime things though...
Yeah this'd likely looks similar to most of our other sanitizer work which would involve building and shipping the runtime support libraries for select platforms and then having -Z
flags in rustc that configures LLVM's pass manager appropriately and then also links the runtime libs, probably not the hardest thing to do but probably also not super trivial.
There I think is some basic profiling support already with -Zprofile
, but I would suspect that it's not trivially usable
oh looks like -Zprofile
may be one of the three mechanisms in llvm for coverage, and it may be the wrong one
In the Wasmtime meeting today we (@Alex Crichton, @Chris Fallin, @Till Schneidereit) talked a bit about fuzzing: what I took away is that the Wasm SIMD fuzzing should be turned on once we finish the Wasm SIMD implementation but even when that happens the differential fuzz targets (i.e. vs wasmi) won't cover this feature. Is that right?
I believe so, yeah
Yes, that's right, we would need a Wasm interpreter that supports SIMD; wasmi
doesn't as far as I can tell
And I guess we were sort of all agreeing that it would be great if we could use the spec interpreter for this... but it might be tricky to run this
...tricky from Rust or within our environment, etc.
yeah, calling into Ocaml from Rust would be tricky, but maybe doable? I have no idea what the FFI is like on the ML side
Do we need to call it as a library or can we get away with forking a process to do that?
I wouldn't necessarily consider this a requirement for stabilizing simd though, I think we need to fuzz it at least a little but wasm-smith has us more than covered on that front
ah, well we could fork a process as long as we are able to get the memory and global contents in return
actually that's an interesting idea: build a server process in Ocaml that wraps the spec interpreter, takes Wasm module bytes as input, and returns execution results, in a protocol over a pipe or something
running the spec interpreter on oss-fuzz would be weird though, I'm not sure if we have tight control over the environment the fuzzed binaries are run within, you'd have to look into oss-fuzz for more details on that
I wouldn't necessarily consider this a requirement for stabilizing simd though
Yeah, I'm just thinking about what is the best possible end state
currently I only know we have tight control over the build environment
like, you mean they might not let us open ports, etc.?
I'm sure it's at least somewhat possible though, and most of the works is probably just building the server process in ocaml lol
because we can certainly build the spec interpreter binary...
completely harebrained idea: somehow translate the spec interpreter, or the core (opcode-matching) parts of it, to Rust? I have no idea how regular its implementation is and how easy it would be to parse it
nah I'm just not sure how they actually run the binary. I thought it was just "download the binary and run it" which gives us no control over the environment
nose goes
well, I see a Dockerfile in there so I assumed that is what was building the artifacts?
nose goes
I am booked out to checks calendar 2024, but I can slot this in sometime after that :-)
in there = https://github.com/google/oss-fuzz/tree/master/projects/wasmtime
I think you'd basically just want to double-check what the running environment is in oss-fuzz, I really don't know myself, i just suspect it's probably not "vanilla"
yeah
yeah the dockerfile there is for building, and I don't think it's used for running but I could be wrong
there must be at least some mechanism to get files in place, for fuzzers that want more complex install environments? or maybe not
and there's the potential they sandbox things somehow too so one can't exec (seccomp or similar)
tbh the best comparison is probably node at this point, I think they've got everything necessary implemented
s/best/easiest/
another thought: it might be ok (not ideal, but ok) if we have a fuzzing mode that requires some additional environment and setup that oss-fuzz can't provide, as we can still run this elsewhere (e.g., the CI machines in the background)
(an aside: does anyone know how to fix -fsanitize-coverage=trace-pc-guard is no longer supported by libFuzzer. Please either migrate to a compiler that supports -fsanitize=fuzzer or use an older version of libFuzzer
before I go off trying to figure out how to fix it?)
Seen when attempting to run: cargo +nightly fuzz run differential
I sometimes run cargo fuzz
with -s none
to turn off all sanitizers, to get a faster build turnaround when debugging a fuzz crash
imho the sanitizers are less important when fuzzing Rust, at least when running locally, as the asserts are the most important oracle (others please correct me if that's not true!)
I get: error: 'none' isn't a valid value for '--sanitizer <sanitizer>' [possible values: address, leak, memory, thread]
weird, how old is your cargo-fuzz
?
0.5.2?
Ah, I'm on 0.8.0:
cfallin@xap:~/work/regalloc.rs$ cargo fuzz run -s none regalloc2
Compiling regalloc2 v0.0.1 (/home/cfallin/work/regalloc2)
Compiling regalloc v0.0.31 (/home/cfallin/work/regalloc.rs/lib)
Compiling minira-util v0.1.0 (/home/cfallin/work/regalloc.rs)
^C Building [========================> ] 53/57: regalloc2, regalloc, minira-util
cfallin@xap:~/work/regalloc.rs$ cargo fuzz --version
cargo-fuzz 0.8.0
oh... latest is at 0.10.2...
and that works great.
Chris Fallin said:
another thought: it might be ok (not ideal, but ok) if we have a fuzzing mode that requires some additional environment and setup that oss-fuzz can't provide, as we can still run this elsewhere (e.g., the CI machines in the background)
the downside here is that we have to build all the infrastructure necessary to dedupe crashes, monitor fuzzing processes and respawn them after they find crashes, etc and this is a bunch of work that oss-fuzz already does for us
I mentioned in the meeting today that it didn't seem impossible to use OCaml's FFI to call in to the spec interpreter from Rust. Let me describe a possible plan and I'm interested to hear how feasible this all sounds (esp. from people with more Rust/FFI expertise):
It would be ideal if all of that could get wrapped up into a wasm-spec-interpreter
crate so that we could use it in the fuzzer...
That all sounds reasonable!
An update on this: I tried out the approach above and it works! Well... at least for int
types :grinning:
I'll try to get more types working before I share the proposed crate
Great news! Looking forward to seeing this!
Others will probably appreciate having "actual Wasm spec interpreter as a Rust crate" as well; the ecosystem of wasm interpreters on crates.io is kinda haphazard right now afaict
Well, after talking to @Alex Crichton about this I just included the crate in the Wasmtime repository. Here is the current state of things: https://github.com/bytecodealliance/wasmtime/pull/3124
@Chris Fallin , @fitzgen (he/him), @Alex Crichton: I think the main problem right now with the PR above is that the wasm-spec-interpreter crate only builds in a certain environment. To solve this, the best I can come up with is to always build the crate but detect during build.rs if the right tools are available and build the OCaml library if they are. If they are not, then set a feature flag and in lib.rs implement the interpret
function by immediately panicking. So the crate should always build but will crash at runtime if the OCaml/Linux bits aren't there. Thoughts?
That seems like an OK compromise, yeah. I guess we already do something similar for OpenVINO (detect if present at build time, still build without it)
sounds fine to me
agreed sounds good
Well, I forgot a crucial detail so I'm not sure this will work: I can detect if the tools are available, set a feature flag, and use this to compile a panicking interpret
function but feature flags set in build.rs
don't affect dependencies, IIRC. So the ocaml-sys
crate still tries to build and fails. Any ideas?
https://github.com/bytecodealliance/wasm-tools/pull/314 may be of interest here in generating more modules that get past instantiation in theory. I still think there's a lot of work to be done on the instruction side of things though where we're more intelligent about generating instructions that aren't super likely to just always trap around memory
@Andrew Brown looks like the oss-fuzz build failed last night -- https://oss-fuzz-build-logs.storage.googleapis.com/index.html#wasmtime
Step #4: Compiling cpp_demangle v0.3.2
Step #4: Compiling crossbeam-channel v0.5.1
Step #4: Compiling quote v1.0.9
Step #4: Compiling aho-corasick v0.7.18
Step #4: Compiling jobserver v0.1.22
Step #4: Compiling getrandom v0.2.3
Step #4: error: failed to run custom build command for `wasm-spec-interpreter v0.1.0 (/src/wasmtime/crates/fuzzing/wasm-spec-interpreter)`
Step #4:
Step #4: Caused by:
Step #4: process didn't exit successfully: `/src/wasmtime/target/release/build/wasm-spec-interpreter-e74f205a2f27f8b8/build-script-build` (exit status: 101)
Step #4: --- stdout
Step #4: cargo:rerun-if-changed=ocaml/interpret.ml
Step #4: cargo:rerun-if-changed=ocaml/Makefile
Step #4: make -C spec/interpreter libopt
Step #4: make[1]: Entering directory '/src/wasmtime/crates/fuzzing/wasm-spec-interpreter/ocaml/spec/interpreter'
Step #4: ls binary/decode.ml binary/decode.mli binary/encode.ml binary/encode.mli binary/utf8.ml binary/utf8.mli exec/eval.ml exec/eval.mli exec/eval_numeric.ml exec/eval_numeric.mli exec/f32.ml exec/f32_convert.ml exec/f32_convert.mli exec/f64.ml exec/f64_convert.ml exec/f64_convert.mli exec/float.ml exec/i32.ml exec/i32_convert.ml exec/i32_convert.mli exec/i64.ml exec/i64_convert.ml exec/i64_convert.mli exec/int.ml exec/numeric_error.ml host/env.ml host/spectest.ml main/flags.ml main/main.ml runtime/func.ml runtime/func.mli runtime/global.ml runtime/global.mli runtime/instance.ml runtime/memory.ml runtime/memory.mli runtime/table.ml runtime/table.mli script/import.ml script/import.mli script/js.ml script/js.mli script/run.ml script/run.mli script/script.ml syntax/ast.ml syntax/free.ml syntax/free.mli syntax/operators.ml syntax/types.ml syntax/values.ml text/arrange.ml text/arrange.mli text/lexer.mli text/lexer.mll text/parse.ml text/parse.mli text/parser.mly text/print.ml text/print.mli util/error.ml util/error.mli util/lib.ml util/lib.mli util/sexpr.ml util/sexpr.mli util/source.ml util/source.mli valid/valid.ml valid/valid.mli \
Step #4: | sed 's:\(.*/\)\{0,1\}\(.*\)\.[^\.]*:\2:' \
Step #4: | grep -v main \
Step #4: | sort | uniq \
Step #4: >wasm.mlpack
Step #4: echo >_tags "true: bin_annot"
Step #4: echo >>_tags "true: debug"
Step #4: echo >>_tags "<{util,syntax,binary,text,valid,runtime,exec,script,host,main}/*.cmx>: for-pack(Wasm)"
Step #4: ocamlbuild -lexflags -ml -cflags '-w +a-4-27-42-44-45 -warn-error +a-3' -I util -I syntax -I binary -I text -I valid -I runtime -I exec -I script -I host -I main -libs bigarray -quiet wasm.cmx
Step #4: + /usr/bin/ocamldep -modules syntax/ast.ml > syntax/ast.ml.depends
Step #4: File "syntax/ast.ml", line 156, characters 14-15:
Step #4: Error: Syntax error
Step #4: Command exited with code 2.
Step #4: Makefile:91: recipe for target '_build/wasm.cmx' failed
Step #4: rm wasm.mlpack _tags
Step #4: make[1]: Leaving directory '/src/wasmtime/crates/fuzzing/wasm-spec-interpreter/ocaml/spec/interpreter'
Step #4: Makefile:28: recipe for target 'spec/interpreter/_build/wasm.cmxa' failed
Step #4:
Step #4: --- stderr
Step #4: Cloning into 'ocaml/spec'...
Step #4: make[1]: *** [_build/wasm.cmx] Error 10
Step #4: make: *** [spec/interpreter/_build/wasm.cmxa] Error 2
Step #4: thread 'main' panicked at 'Failed to build the OCaml library using 'make'.', crates/fuzzing/wasm-spec-interpreter/build.rs:57:5
Step #4: note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
Step #4: warning: build failed, waiting for other jobs to finish...
Step #4: error: build failed
Step #4: Error: failed to build fuzz script: "cargo" "build" "--manifest-path" "/src/wasmtime/fuzz/Cargo.toml" "--target" "x86_64-unknown-linux-gnu" "--release" "--features" "peepmatic-fuzzing experimental_x64" "--bins"
Step #4: ********************************************************************************
Step #4: Failed to build.
Step #4: To reproduce, run:
Step #4: python infra/helper.py build_image wasmtime
Step #4: python infra/helper.py build_fuzzers --sanitizer address --engine libfuzzer --architecture x86_64 wasmtime
Step #4: ********************************************************************************
Finished Step #4
ERROR
ERROR: build step 4 "gcr.io/oss-fuzz/wasmtime" failed: step exited with non-zero status: 1
is that an issue perhaps where ocaml is too old?
Step #4: File "syntax/ast.ml", line 156, characters 14-15:
Step #4: Error: Syntax error
oh wow it looks super old, like 4.02 may be pulled in?
yeah, when I ran the oss fuzz image in docker I saw that 4.02 was pulled in
yup
Step #1: Setting up ocaml-findlib (1.5.5-2build1) ...
Step #1: Setting up ocaml-compiler-libs (4.02.3-5ubuntu2) ...
Step #1: Setting up ocaml-interp (4.02.3-5ubuntu2) ...
Step #1: Setting up ocaml-nox (4.02.3-5ubuntu2) ...
and I thought, "hm, this might be a problem..." :grinning:
well, I wonder if there is a way to use opam to upgrade ocaml or something
the issue is that they're using a really old Ubuntu as the base for the oss-fuzz image
16.x
is there a newer oss fuzz image?
Looks like there is no newer oss fuzz image, but I think the following sequence will update the tools to 4.12:
sh <(curl -sL https://raw.githubusercontent.com/ocaml/opam/master/shell/install.sh)
opam init --disable-sandboxing
opam install ocamlbuild
eval $(opam env --switch=default)
Inside the oss fuzz image that is enough to compile the spec interpreter.
Unfortunately that has multiple "read from stdin" scripts
eh that's fine imo
:+1: I would need to figure out how to pass in the right sequence of <enter> y <enter> ...
--do you have a preference on how to do that?
uh... unsure lol
when in doubt sometimes yes | the_script
works
but if that doesn't work I'd root around for some sort of "please assume yes" cli switch
@Alex Crichton, I see that https://github.com/google/oss-fuzz/pull/6205 got merged; how do we see if the build now passes? Do we have to wait for an e-mail telling us it crashed or is there some other way to inspect what is going on?
I got an email about another build failure, but I think it's because the changes weren't included
I go to oss-fuzz and hit on build logs
and it should have logs for wasmtime
I don't see that:
image.png
or you meant build status?
Ok, yeah, if I navigate around in there I can see the logs for the latest build and it is still complaining about a syntax error
ok
er, sent early.
I did a bit today looking into the spec interpreter timeouts, and my conclusion is that the whole thing is and probably won't ever be written for performance. I fear that our path to differential fuzzing with the spec interpreter is going to be severly limited given the nature of the spec interpreter.
I was curious, so I played around with Deno's rusty_v8
crate to see how bad it would be to set up differential fuzzing against v8 instead of the spec interpreter. I came up with this and it seems to be working pretty well. When I enabled simd it pretty quickly found https://github.com/bytecodealliance/wasmtime/issues/3216 after I waded through the preexisting fuzz bugs. With the bindings I wrote so far we should have comparisions on instantiation results, comparison on values, and comparisons on memory, which I think is above-and-beyond what we do for both wasmi and the spec interpreter at the moment.
I'm curious how others feel about this. Should we switch from the spec interpreter to v8? Should we try to push on the spec interpreter? I think v8 has the benefit that it's (a) maintained by Deno with rusty_v8
, so we get that for free and (b) it's a fuzzed engine we're unlikely to find bugs in (performance or otherwise). Personally I feel that we'll get 99% of the benefit of differential fuzzing by just fuzzing against something other than ourselves. While I think it's nice to fuzz against the spec interpreter I don't think it brings the lion's share of the benefit.
Interesting -- thank you for digging into this, first of all!
I think there is definitely a lot of value in fuzzing against "peers" -- especially V8 I expect to be very, very closely checked w.r.t. the spec. I'll note that we already had fuzzing against wasmi
as well, so if we're going to mainly focus on this sort of fuzzing, it's worth evaluating whether we want to keep the latter. (Probably not, since it doesn't do SIMD, for starters.)
I am curious if there are any really easy-to-pick bits of performance in the spec interpreter, though. While (i) we aren't in the business of maintaining it, and (ii) it will certainly want to optimize for clear, unambiguous implementation over any sort of optimization, it seems to me that the folks who do maintain it would be interested in fixing obvious quadratic behavior, and also, fuzzing against "The Spec" is a gold standard and a nice thing to be able to say we do, if we can
I did look a wee bit at what the nested-blocks example was doing and it looked like it had a funky multistage eval step function that prepended Plain
and did some stack munging on every level -- it felt like it might be home to some inefficient n^2 list-mapping but I didn't dig deep enough to really say. Is that the part you were looking at?
yeah that was the same conclusion I reached on the spec interpreter, adding Plain
to new lists in a way that was probably pretty inefficient in terms of list management
Personally I don't want to open a bug on the spec repo, I fear it will get lost to the mists of time or otherwise no one will be able to think of a better way that's "clean enough" for the spec interpreter to use
I do agree though that we don't really need to do differential-execution against multiple implementations, just one should suffice. If the spec interpreter gets further I think we should remove wasmi, and if v8 gets further we should also remove wasmi
fair concern, I too am vaguely scared of crossing a "PL purist" viewpoint that dismisses this if we try to file an issue without a suggested solution; it might be worth playing a bit more with it (by which I mean, I feel like I might do this, in a bit of free time later) though to see if we can offer a constructive suggestion at the same time
I did find it quite easy to reproduce with the interpreter, the input wasm I have in the issue can be changed to just have a start
function and the instantiation clearly takes multiple seconds, and it gets worse by adding more blocks.
jumping ahead a few steps -- in the situation where we get both the spec interpreter to work, and also have your V8 differential fuzzing harness polished and merged -- the question would be: does it make sense to have both? I would argue yes; it's interesting to see if there are disagreements between the spec and the "real world", at least
cool, I will put a bit of time into this later then
nah if the spec interpreter works I don't think v8 is worth it
it's a pretty chonky thing to maintain, even if rusty_v8
does the worst parts for us
eh, that's fair, if the complexity/cost is too high
like I won't disagree it's strictly better to have more fuzzing, but for bang-for-our-buck I'm not sure how much we'd get
I'm actually sort of curious how oss-fuzz budgets CPU time if we add more fuzz targets; do we get a fixed quota per target or per project? in any case if we don't need it badly enough then it's not really good citizenship to burn the cycles shrug
heh for that I have no idea...
FWIW my take on the spec interpreter is that I think the slowdown is this line b/c all the other lists/maps in the Block
case are constant-time, but I could be wrong and it could be related to Label
handling later. Unless the ocaml interpreter does crazy optimizations though List32.length
and such functions were also O(n) which was about the time I lost hope for making that fast
yup I was staring at that exact bit too
OK, so here's my understanding of the quadratic behavior: the evaluator step function is designed to step the "configuration" (stack of values, and a list of possibly nested terms that represent remaining instructions) exactly one step, no matter how deep the label stack is. The way that a step
works when there are many nested labels on the stack is that we recurse down to the innermost label's instruction list, step its configuration once, then walk back out, rebuilding the nest of Label
terms up to the root of the function's configuration.
So we start with a config like:
Block (Block (Block (Block (Block ... (code)))))
and this steps to
Label l1 (Plain Block (Block ...))
then
Label l1(Label l2 (Plain Block ...))
and so on.
However each of the steps must go through 1..n recursive step
calls, so we have a total of O(n^2) Ocaml calls and executions of this bit of code.
This is made worse by the handling of the call stack -- it's just a part of the "configuration" as well, so we'll have Label (Label (Label ... (Frame (Label (Label (Label ... ))))))
with 1000
frames in the 1000-deep-recursion-in-nested-blocks timeout example
the fundamental bit that's expensive is the way that the step walks all the way back out the tree of terms and rebuilds it for each inner step; if the inner step did a step to completion then it would be efficient; but I suspect that would break an "execute for exactly one unit of time so as not to run forever" sort of fuel-limiting mechanism
fixing this might not be so bad if we don't care about that; but I'd want to spend a bit more time understanding it first
(fwiw, perf
on the interpreter binary showed ~15% of time in just that one line lined above; and ~50% of time in GC-related code, because of the reallocation on each rebuild of the config)
(I'll summarize this on the github issue for the timeout)
... and I went and did the thing: https://github.com/cfallin/spec/commit/817f8e84f2fa289723e724553e74d6ce13898ec8
Just catching up on this thread: wow! nice analysis and good fix. What are you thinking between merging upstream vs merging into https://github.com/bytecodealliance/wasm-spec-mirror?
So I'm cleaning it up a bit and I'll go ahead and create a PR on spec
and see what happens -- at worst it will spawn discussion and help to clarify "very simple theoretically correct interpreter" vs. "actually usable interpreter without quadratic behavior" as a position taken by the folks who maintain it :-)
https://github.com/WebAssembly/spec/pull/1354
Indeed, great work on figuring this out and fixing it!
My take is that it's fine for the spec interpreter to be written for readability and maintainability over speed—but not for it to execute code in a way that has a different algorithmic complexity class from what production implementations would be expected to have. ISTM that otherwise it just says next to nothing about implementability of proposals, which seems highly unfortunate. Not sure if that'll be the common view, of course
Hmm, it seems I don't have push access to wasm-spec-mirror
, and the GitHub UI is not letting me create a PR on it when I also have an open one on WebAssembly/spec (unless I'm missing a nonobvious button somewhere)
@Till Schneidereit or @Andrew Brown could you grant me permissions and I'll just push a branch for now?
... ah, nevermind, I had the wrong base branch selected
I just added wasmtime-core and cranelift-core as repo maintainers
there we go, PR onto fuzzing
branch: https://github.com/bytecodealliance/wasm-spec-mirror/pull/1
Ok, merged... let me create a PR to make sure we pull that branch when fuzzing: https://github.com/bytecodealliance/wasmtime/pull/3221
Oh, I just did that too, sorry for racing!
heh, I should have checked :grinning:
lol, well take your pick
(I was going to ask you if you were going to do it and then though, "oh, I can just push that real quick")
let's use yours since it creates a constant up top
sure, either way :-)
@Andrew Brown fyi, it's looking like it probably will not be very feasible to remove the quadratic behavior from the spec interpreter: https://github.com/WebAssembly/spec/pull/1354 (basically we got an "interpreter should be direct translation of small-step semantics" answer)
I had an alternate thought though: we could still potentially use it for individual instruction semantics (for especially SIMD this seems valuable). Would it make sense to tweak wasm-smith to generate very simple programs (e.g. no control flow) and use the infra for that?
hm, yeah
not a bad idea
that's sort of a separate use-case than fuzzing against a fast interpreter, sort of a breadth vs. depth thing (by running larger programs we get less coverage of e.g. different bit patterns in inputs)
an extension on that would be to configure wasm-smith to avoid generating cases that cause the quadratic slowdown
what a pain this turned out to be :grinning:
"just fuzz against the spec" they said, "how hard could it be" they said...
I think no cnotrol flow (including no calls) is enough to ensure no quadratic behavior
that's probably pretty easy to add to the configuration trait; any interest on your part in trying this? (I can throw it on my long-term todo list otherwise but my todo list is also growing quadratically)
well, I was thinking about taking a look at the v128 stuff before I go on sabbatical here in a few weeks, I could look at it when I do that
awesome!
To close the loop on this -- I created https://github.com/bytecodealliance/wasmtime/issues/3251 to track it
Last updated: Dec 23 2024 at 13:07 UTC